1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 | Some rules of production: ------ ab ------ bc ------- cab (basic rules) A => B B => C C => AB x => x′ x => y y => z ----------- sub -------------- cut (structural rules) wxy => wx′y x => z Maybe you don't have cut, or have a separate relation =>* with a similar looking cons rule (and a nil rule). Depends what you want. A derivation: ------ bc B => C ---------- sub ABC => ACC Some LK production rules: Both sides of a sequent are sets of well formed formulae, so no need for structural rules. There are no axioms in LK, at least by my understanding of ldlework's definition. Γ => Δ,A,B Γ,A => Δ ---------- init ---------- ∨r --------- ¬r Γ,A => A,Δ Γ => Δ,A∨B Γ => Δ,¬A A proof: ------ init A => A ------- ¬r => A,¬A ------- ∨r => A∨¬A So, => A∨¬A is a theorem of LK. A∨¬A is just syntax in LK. We can notice that it forms a theorem, but it is not a theorem alone. This means that LK validates the principle of excluded middle. The principle states that every proposition is either true or false. A formal system validating the principle of excluded middle is suitable for modelling situations where everything is decidable. Principles carry extra-mathematical meaning, the kind a strict formalist would reject and a platonist would call a “law”. A principle is not tied to a specific formal system, as axioms and theorems are. A principle can be considered in a range of formal systems, and we can judge whether each system validates the principle. Systems which satisfy the same principles will come to the same conclusions, but perhaps by different means and with different syntaxes. |