# First Order Logic with Athena

2020-06-07, updated 2020-06-07 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 that can be downloaded at Proof Central.

## 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.

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