Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion On a proof theoretical semantics for bilateral classical logic Yoriyuki Yamagata National Institute of Advanced Industrial Science and Techonology (AIST) 2019/11/30 Collaborated with Ukyo Suzuki (Picolab Co.,Ltd.)
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Full-blooded theory of meaning A full-blooded theory [Dummett, 1976] of meaning explains a speaker’s understanding of language, how it manifests by observable action by a “molecular” way
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Problem of truth conditinal semantics Truth conditional semantics suﬀers from truth value does not show the speaker’s understanding truth value may not be decidable, therefore its knowledge may not be manifested Davidson’s approach leads “Holism” [Davidson, 2001] Therefore cannot be regarded as a full-blooded theory of meaning
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Dummett’s Challenge Classical logic seems to have a strong connection to truth conditional semantics, namely, bivalence. Problem Can we ﬁnd a full-blooded theory of meaning which justiﬁes classical logic?
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Proof theoretical semantics (PTS) The meaning of a sentence is its formal derivation A possible candidate of full-blooded theory of semantics Also related to the use theory of meaning and inferentialism [Brandom, 1994] Problem Formal derivations are “holistic”
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Approach using natural deduction Proposal A pair of introduction/elimination rules gives a meaning Impose a certain “harmony” between the intro./elimination pair Remark Other connectives do not involve an intro./elimination pair, thus molecularity is preserved Harmony guarantees a certain “soundness” of the deductive practice.
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Formalizing harmony Global approach [Schroeder-Heister, 2016] A “canonically valid proof” = a proof built by an introduction rules A “valid proof” = a proof reducible to a canonically valid proof Soundness of a deductive system = all proofs are valid proofs Local approach A successive pair of introduction/elimination rules can be eliminated
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Problem of classical logic Problem (Dummett) [¬A] . . . . ⊥ ¬¬A A RAA =⇒ . . . . A but how? There are many A which cannot be derived without RAA.
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Justiﬁcation of the logical rules of BCL Logical rules have (local) harmony Example +A −B −A → B +A =⇒ +A
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Justiﬁcation of the coordination rules of BCL Example (Problematic coordination rules) [+A] ⊥ +A [−A] ⊥ −A Rummﬁtt argued that it is impossible to justify the coordination rules by a purely proof theoretical mean [Rumﬁtt, 2008]
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Diﬃculty of jutiﬁcation of the coorination rules A possible idea is regarding RAA as an introduction rule and contradiction as an elimination rule Problem [Suzuki, 2015] RAA refers +A to derive −A and −A to derive +A. Therefore, meaning is circularly deﬁned. Local harmony also has diﬃculties. Proposal (Our contribution) Braking this circularly by using a ﬁxed point construction
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Validity of BCL Proposal Meaning conferring The introduction rules and RAA Derivative The elimination rules and the contradiction rule
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Knaster-Tarski Theorem Theorem Let L be a complete lattice. Let F : L → L be a monotone map, that is, x ≤ y =⇒ F(x) ≤ F(y) Then, F has a ﬁxed point F(x) = x Proof. Omitted, but we remark that the usual proof requires impredicative construction, and the speaker does not know whether a predicative proof exists or not.
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Example: ±A → B Deﬁnition The set of canonically valid proofs of implication is deﬁned as: +A → B := ( +A →+A→B +B ) ∪ −A → B ∗ −A → B := ( +A ⊗−A→B −B ) ∪ +A → B ∗ Remark Apparent circularly is avoided by the ﬁxed point construction
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Soudness and Completeness Theorem (Soundness) All BCL proofs are valid Theorem (Completeness) All conclusion of valid proofs can be derived by BCL proofs Proof. Omitted, but note that the completeness requires a classical reasoning. On the other hand, soundness can be proven without using the law of the excluded middle
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Impredicativity 1 Constructivists often do not accept impredicative arguments 2 However, our goal is not to persuade a constructivist but explain the classical deductive practice to who already accepts classical mathematics (in particular, impredicative argument) 3 We note that our argument does not superﬁcially use classical reasoning, therefore illuminates the rˆ ole of the classical reasoning principles.
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Manifestability 1 Our canonical validity is not decidable (in the sense of the usual mathematical sense) 2 However, as we proved, BCL is sound and complete. Therefore, someone who always follows BCL can be judged to have a grasp of the meaning. 3 Further, Prawitz’s original notion of validity is also undecidable, as shown in the next slides.
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Undecidability of validity (Example) I Deﬁnition T : Turing machine s0 , s1 , . . . : states ω : the terminal state Rs : the computation from s terminates Deﬁnition (Basic system) Axiom Rω Rule Rs ⊢ Rs′ if s′ reduces s Logical rules Usual logical rules for →
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Undecidability of validity (Example) II Example (Strange elimination rule and reduction rule) Rs′ → Rs Rs Rs′ . . . . Rs Rs′ → Rs Rs ⇝ Rs′′ Rs′ Rs′′ → Rs′ Rs′ . . . . Rs where s′ reduces s and s′′ reduces s′. This reduction only terminates when the computation from s terminates
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Conclusion We give a notion of validity to Rummﬁtt’s bilateral classical logic (BCL) Our notion of validity can justify all rules of BCL, including the coordination rules To overcome an apparent circularly for deﬁning the validity of BCL, we use Knaster-Tarski’s ﬁxed point theorem We justify the use of the ﬁxed point theorem by distinguishing explanation from persuasion Our notion of validity is undecidable, but we give a suﬃcient condition of validity, that is, all BCL deduction is valid
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Reference I Brandom, R. (1994). Making It Explicit: Reasoning, Representing, and Discursive Commitment. Cambridge: Harvard University Press. Davidson, D. (2001). Inquiries into truth and interpretation: Philosophical essays, volume 2. Oxford University Press.
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Reference II Dummett, M. (1976). What is a theory of meaning? (ii). In Evans, G. and McDowell, J., editors, Truth and Meaning: Essays in Semantics., pages 67–137. Oxford: Clarendon Press. Rumﬁtt, I. (2000). Yes and no. Mind, 109(436):781–823. Rumﬁtt, I. (2008). Co-ordination principles: A reply. Mind, 117(468):1059–1063.
Yamagata Dummett’s Challenge Proof theoretical semantics Bilatetal classical logic Validity of BCL Philosophical discussion Reference III Schroeder-Heister, P. (2016). Open problems in proof-theoretic semantics. In Piecha, T. and Schroeder-Heister, P., editors, Advances in Proof-Theoretic Semantics, pages 253–283. Cham: Springer International Publishing. Suzuki, U. (2015). Falsiﬁcationism and bilateralism. Inferentialism Workshop. http://www.academia.edu/19114409/ Bilateralism_and_Falsificationism. Accessed 29 Oct 2019.