Why "Tonk" is Nonsensical -- and Paradoxes aren't: an Approach in a Typed Sequent Calculus System

(Logic, English)

onk is the notorious connective Prior used in his famous paper from 1960 ("The Runabout In-ference-Ticket") to give a reductio ad absurdum-argument against the idea of proof-theoretic semantics, i.e. the idea that all there is to the meaning of logical connectives are the rules of inference that govern their use. If that was true, Prior argues, we could just as easily invent a connective with completely arbitrary rules and state that this connective was meaningful, after all we had its rules. In the case of tonk the rules consist of an introduction rule which resembles the one for disjunction ("from A one can derive A tonk B") and an elimination rule which resembles the one for conjunction ("from A tonk B one can derive B"). Thus, it would be possible to derive arbitrary B from arbitrary A, which would trivialize the notion of logical consequence and, in the view of proof-theoretic semantics, the notion of meaning. As this posed a serious threat, in the following decades a vast amount of literature was published that tried to make out a necessary condition for rules, which would keep the "good" connectives while ruling out connectives like tonk.

There is another reason why tonk is a challenging connective: it displays proof-theoretic parallels to paradoxical connectives since with both it is possible to derive absurdity with a proof that is in principle non-normalizable. However, although both are non-standard connectives, intuitively we want to ascribe some meaning to paradoxical connectives, whereas tonk is plain nonsense by its own definition. Therefore, it would be desirable to spell out this intuition proof-theoretically. In this talk I will show how this is possible not only for natural deduction systems but also for sequent calculi where the distinction between tonk and paradoxes is not as easy to draw because notions like reduction procedures are missing. These can be retrieved, though, by creating typed rules for sequent calculus and thus, by using the notion of term reduction from lambda-calculus. Thereby, we are able to show the proof-theoretical distinction between meaningful and not meaningful non-standard phenomena and thus, combine syntax and semantics in a fruitful way.

Chair: Tobias Koch

Time: 14:00-14:30, 14 September 2018 (Friday)

Location: SR 1.006

Sara Ayhan

(Ruhr-University Bochum, Germany)

Since March 2018 I am a PhD student supervised by Heinrich Wansing at the "Logic and Epistemology"-department at the Ruhr-University Bochum. Before that I obtained the degree of 1st state exam in philosophy, English and history in 2015 with a thesis about Donald Davidson's conception of truth and the Master of Arts degree in philosophy in 2018 at the RUB. During these studies I also spent a semester abroad at the University of Adelaide, South Australia. I wrote my Master's thesis about the treatment of paradoxes in proof-theoretic semantics and continue this work in my PhD project with the focus on consequence relations and identity of proofs.

© 2021 SOPhiA. All rights reserved.
Last update: 2014-04-01.