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.

Table 1: Athena Notation for Natural Deduction in Propositional Logic
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)
   (!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
\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
 

Author: Joseph Vidal-Rosset

Date: 2020-06-07 dim. 17:37

Blog: https://wwww.vidal-rosset.net

Made with Emacs 26.3 (Org mode 9.3.7) and Org export head (Many thanks to Ivan Tadeu Ferreira Antunes Filho!;)