# First Order Logic with Athena

2021-03-19, updated 2023-05-22 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
\begin{prooftree} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$A$} \noLine \UnaryInfC{$\vdots$} \noLine \UnaryInfC{$\bot$} \RightLabel{$\scriptsize{\to I, 1}$} \UnaryInfC{$\lnot A$} \end{prooftree}
> assert (A ==> false)
(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
\begin{prooftree} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$A$} \noLine \UnaryInfC{$\vdots$} \noLine \UnaryInfC{$B$} \RightLabel{$\scriptsize{\to I, 1}$} \UnaryInfC{$A \to B$} \end{prooftree}
> 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}
\begin{prooftree} \AxiomC{$B$} \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
\begin{prooftree} \AxiomC{$A \lor B$} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$A$} \noLine \UnaryInfC{$\vdots$} \noLine \UnaryInfC{$C$} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$B$} \noLine \UnaryInfC{$\vdots$} \noLine \UnaryInfC{$C$} \RightLabel{$\scriptsize{\lor E, 1}$} \TrinaryInfC{$C$} \end{prooftree}
> 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
\begin{prooftree} \AxiomC{$A$} \AxiomC{$B$} \RightLabel{$\scriptsize{\land I}$} \BinaryInfC{$A \land B$} \end{prooftree}
> 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
\begin{prooftree} \AxiomC{$A \land B$} \RightLabel{$\scriptsize{\land E}$} \UnaryInfC{$A$} \end{prooftree} \begin{prooftree} \AxiomC{$A \land B$} \RightLabel{$\scriptsize{\land E}$} \UnaryInfC{$B$} \end{prooftree} \begin{prooftree} \AxiomC{$A \land C \land B$} \RightLabel{$\scriptsize{\land E}$} \UnaryInfC{$C$} \end{prooftree}
> 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
\begin{prooftree} \AxiomC{$A \to B$} \AxiomC{$B \to A$} \RightLabel{$\scriptsize{\land I}$} \BinaryInfC{$A \leftrightarrow B$} \end{prooftree}
> 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
\begin{prooftree} \AxiomC{$A \leftrightarrow B$} \RightLabel{$\scriptsize{\land E}$} \UnaryInfC{$A \to B$} \end{prooftree} \begin{prooftree} \AxiomC{$A \leftrightarrow B$} \RightLabel{$\scriptsize{\land E}$} \UnaryInfC{$B \to A$} \end{prooftree}
> 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)
\begin{prooftree} \AxiomC{$\bot$} \RightLabel{$\scriptsize{\bot E}$} \UnaryInfC{$C$} \end{prooftree}
> assert false
(!from-false C);;

The sentence
false
has been added to the assumption base.

Theorem: C

• Double negation elimination (rule for classical logic)
\begin{prooftree} \AxiomC{$\scriptsize{1}$} \noLine \UnaryInfC{$\lnot A$} \noLine \UnaryInfC{$\vdots$} \noLine \UnaryInfC{$\bot$} \RightLabel{$\scriptsize{DN, 1}$} \UnaryInfC{$A$} \end{prooftree}
> 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


Made with Emacs 29.0.50 (Org mode 9.5) and with org-export-head, a blog exporter.

The css file of this blog is mainly the result of Zhitao Gong's work.