Speaker

# Barteld Kooi

University of Groningen

### Talks at this conference:

Friday, 16:55, J335 |
## Constructing Harmony |

Within the context of Gentzen-calculi for classical propositional logic we present an algorithm that constructs a left rule from a right rule (and vice versa). First, we show that the algorithm is correct. Second, we use our algorithm to analyse the relation between proof-theoretical semantics (the meaning of an operator is given by its inference rules) and model-theoretical semantic (the meaning of an operator is given by its truth- and falsity-conditions). Third, we use our algorithm to study the concept of harmony and show what is wrong with Prior’s pair of rules for In Gentzen-calculi for classical logic every operator has a left rule and a right rule. Bearing Prior’s challenge in mind, it has often been noted (first by Gentzen himself) that left rules and right rules are dependent, but as yet it is still under debate how this relation must be understood. In the context of natural deduction systems, Prawitz proposes his “Inversion Principle” to make this relation more precise. Crudely speaking, his principle says that an introduction rule followed by an elimination rule can never lead to anything beyond the original premises. Using our |