First Order Logic with Athena
2021-03-19, updated 2024-03-01 next - previous
This note is about Athena, a language invented by Konstantine Arkoudas, for expressing proofs and computation.
Athena is also a First Order Logic proof checker. To download Athena and to be informed about Athena, go to Athena Foundation web page.
1. Natural Deduction for Classical Propositional Logic
First, Table _1 provides, in Athena language, the expressions of logical rules for classical propositional logic. Second, the usual diagram of each rule in natural deduction is reflected in the reproduction of Athena’s inputs-outputs. _1
| Athena | true | false | ~A | A ==> B | A | B | A & B | A <==> B |
| usual notation | \(\top\) | \(\bot\) | \(\lnot A\) | \(A \to B\) | \(A \lor B\) | \(A \land B\) | \(A \leftrightarrow B\) |
| I-rules | !dn | !by-contradiction | assume | !either | !both | !equiv | |
| usual notation | \(DN, n\) | \(\lnot I, n\) | \(\to I, n\) | \(\lor I\) | \(\land I\) | \(\land I\) | |
| E-rules | !from-false | !absurd | !mp | !cases | !conj-elim | !left-iff !right-iff | |
| usual notation | \(\bot E\) | \(\lnot E\) | \(\to E\) | \(\lor E\) | \(\land E\) | \(\land E\) |
Each Athena input-output is going to be presented like the following declaration of terms that is necessary to Athena before developing proofs.
> declare A , B , C : Boolean;; New symbol A declared. New symbol B declared. New symbol C declared.
- Negation introduction
> assert (A ==> false) (!by-contradiction (~ A) (A ==> false));; The sentence (if A false) has been added to the assumption base. Theorem: (not A)
Negation elimination:
\begin{prooftree} \AxiomC{$\lnot A$} \AxiomC{$A$} \RightLabel{$\scriptsize{\lnot E}$} \BinaryInfC{$\bot$} \end{prooftree}
> assert (~ A) A
(!absurd (~ A) A);;
The sentence
(not A)
has been added to the assumption base.
Term: A
Theorem: false
- Conditional introduction
> assert B
(assume A
(!claim B));;
The sentence
B
has been added to the assumption base.
Theorem: (if A B)
Conditional elimination
\begin{prooftree} \AxiomC{$A \to B$} \AxiomC{$A$} \RightLabel{$\scriptsize{\to E}$} \BinaryInfC{$B$} \end{prooftree}
> assert (A ==> B) assert A
(!mp (A ==> B) A);;
The sentence
(if A B)
has been added to the assumption base.
The sentence
A
has been added to the assumption base.
Theorem: B
Disjunction introduction
\begin{prooftree} \AxiomC{$A$} \RightLabel{$\scriptsize{\lor I}$} \UnaryInfC{$A \lor B$} \end{prooftree}
> assert A (!either A B);; The sentence A has been added to the assumption base. Theorem: (or A B) > assert B (!either A B);; The sentence B has been added to the assumption base. Theorem: (or A B)
- Disjunction elimination
> assert (A | B) , (A ==> C), (B ==> C) (!cases (A | B) (A ==> C) (B ==> C));; The sentence (or A B) has been added to the assumption base. The sentence (if A C) has been added to the assumption base. The sentence (if B C) has been added to the assumption base. Theorem: C
- Conjunction introduction
> assert A , B
(!both A B);;
The sentence
A
has been added to the assumption base.
The sentence
B
has been added to the assumption base.
Theorem: (and A B)
- Conjunction elimination
> assert (A & B) (!conj-elim A (A & B));; The sentence (and A B) has been added to the assumption base. Theorem: A > assert (A & B) (!conj-elim B (A & B));; The sentence (and A B) has been added to the assumption base. Theorem: B > assert (A & C & B) (!conj-elim C (A & C & B));; The sentence (and A (and C B)) has been added to the assumption base. Theorem: C
- Biconditional introduction
> assert (A ==> B), (B ==> A) (!equiv (A ==> B) (B ==> A));; The sentence (if A B) has been added to the assumption base. The sentence (if B A) has been added to the assumption base. Theorem: (iff A B)
- Biconditional elimination
> assert (A <==> B) (!left-iff (A <==> B));; The sentence (iff A B) has been added to the assumption base. Theorem: (if A B) > assert (A <==> B) (!right-iff (A <==> B));; The sentence (iff A B) has been added to the assumption base. Theorem: (if B A)
- Falsity constant elimination (Ex Falso Quodlibet, rule for intuitionistic logic)
> assert false
(!from-false C);;
The sentence
false
has been added to the assumption base.
Theorem: C
- Double negation elimination (rule for classical logic)
> assert (~ ~ A), (~ A ==> false)
(!dn (~ ~ A));;
The sentence
(not (not A))
has been added to the assumption base.
The sentence
(if (not A)
false)
has been added to the assumption base.
Theorem: A
