il
This document tries to build up intuitionist (constructive) logic.
• Intuitionist Logic Wikipedia: en.wikipedia.org/wiki/Intuitionistic_logic
• Sequent Calculus Wikipedia Page: en.wikipedia.org/wiki/Sequent_calculus
• Interaction Nets Blog: zicklag.github.io/blog/interaction-nets-combinators-calculus/
• Intuitionist Logic
• Hoare Logic
• Linear Logic
• Proof net
• Proof theory
• Interaction Nets
• Sequent Calculus (we can define our logic in terms of sequent calculus)
• Syntax, Semantics
• combinators : combinatory-logic.md
• Natural deduction: models how we think intuitively. emphasizes introduction and elimination rules.
• Sequent calculus: represents logical arguments through sequents. helps for studying consistency and completeness.
• Hilbert Systems: characterized by a small set of axioms and inference rules.
An inference rule is a rule that, given one sequent (i.e. knowing that something holds from something else), we then know another sequent holds. An example:
cut(⊢P P⊢Q)/(⊢Q)
Which can be read as, "I know P and P implies Q, so using the inference rule 'cut' we know Q"
We can define all of basic logic this way!
It's inherently constructive
Resources
• Intro to linear logic: logicallycoherent.github.io/blog/introduction-to-linear-logic/• Intuitionist Logic Wikipedia: en.wikipedia.org/wiki/Intuitionistic_logic
• Sequent Calculus Wikipedia Page: en.wikipedia.org/wiki/Sequent_calculus
• Interaction Nets Blog: zicklag.github.io/blog/interaction-nets-combinators-calculus/
Topics
• Natural deduction• Intuitionist Logic
• Hoare Logic
• Linear Logic
• Proof net
• Proof theory
• Interaction Nets
• Sequent Calculus (we can define our logic in terms of sequent calculus)
• Syntax, Semantics
• combinators : combinatory-logic.md
Proof Calculus vs Logic
Proof calculus (calculi?) are formal systems and syntax for constructing proofs. They formalize the systems of reasoning that we have. Some examples:• Natural deduction: models how we think intuitively. emphasizes introduction and elimination rules.
• Sequent calculus: represents logical arguments through sequents. helps for studying consistency and completeness.
• Hilbert Systems: characterized by a small set of axioms and inference rules.
Classical Sequent Calculus
A sequent is of the form: $P_1,...,P_n ⊢ Q_1,...,Q_n$ which just implies $P_1 \land ... \land P_n -> Q_1 \vee ... \vee Q_n$. "⊢" is a turnsile. Tao and Delta (Γ,Δ) are used to describe arbitrary formula.An inference rule is a rule that, given one sequent (i.e. knowing that something holds from something else), we then know another sequent holds. An example:
cut(⊢P P⊢Q)/(⊢Q)
Which can be read as, "I know P and P implies Q, so using the inference rule 'cut' we know Q"
We can define all of basic logic this way!
It's inherently constructive