Library hydras.Ackermann.fol

First Order Logic

Original author: Russell O'Connor

This file is Public Domain

First Order Formulas over a language

Record Language : Type := language
{ Relations : Set;
   Functions : Set;
   arityR : Relations → nat;
   arityF : Functions → nat}.

Section First_Order_Logic.

Variable L : Language.

Inductive Term : Set :=
  | var : nat → Term
  | apply : ∀ f : Functions L, Terms (arityF L f) → Term
with Terms : nat → Set :=
  | Tnil : Terms 0
  | Tcons : ∀ n : nat, Term → Terms n → Terms (S n).

Scheme Term_Terms_ind := Induction for Term Sort Prop
  with Terms_Term_ind := Induction for Terms Sort Prop.

Scheme Term_Terms_rec := Minimality for Term Sort Set
  with Terms_Term_rec := Minimality for Terms Sort Set.
Scheme Term_Terms_rec_full := Induction for Term Sort Set
  with Terms_Term_rec_full := Induction for Terms Sort Set.
Inductive Formula : Set :=
  | equal : Term → Term → Formula
  | atomic : ∀ r : Relations L, Terms (arityR L r) → Formula
  | impH : Formula → Formula → Formula
  | notH : Formula → Formula
  | forallH : nat → Formula → Formula.

Definition Formulas := list Formula.
Definition System := Ensemble Formula.
Definition mem := Ensembles.In.

Extensions of the basic language of formulas

Definition orH (A B : Formula) := impH (notH A) B.
Definition andH (A B : Formula) := notH (orH (notH A) (notH B)).
Definition iffH (A B : Formula) := andH (impH A B) (impH B A).
Definition existH (x : nat) (A : Formula) := notH (forallH x (notH A)).

Definition ifThenElseH (A B C : Formula) :=
andH (impH A B) (impH (notH A) C).

Decidability of equality between terms, formulas, ...

Section Formula_Decidability.

Definition language_decidable :=
((∀ x y : Functions L, {x = y } + {x ≠ y }) ×
(∀ x y : Relations L, {x = y } + {x ≠ y }))%type.

Hypothesis language_eqdec : language_decidable.

Lemma term_eqdec : ∀ x y : Term, {x = y } + {x ≠ y }.

Lemma terms_eqdec n (x y : Terms n): {x = y } + {x ≠ y }.

Lemma formula_eqdec : ∀ x y : Formula, {x = y } + {x ≠ y }.

End Formula_Decidability.

Depth Induction

Many functions on term and formulas are not structurally recursive (e.g. because of substitution of variables with terms). In which case, we may use some notion of depth as a measure.

Section Formula_Depth_Induction.

Fixpoint depth (A : Formula) : nat :=
  match A with
  | equal _ _ ⇒ 0
  | atomic _ _ ⇒ 0
  | impH A B ⇒ S (Nat.max (depth A) (depth B))
  | notH A ⇒ S (depth A)
  | forallH _ A ⇒ S (depth A)
  end.

Definition lt_depth (A B : Formula) : Prop := depth A < depth B.

Definition Formula_depth_ind :
  ∀ P : Formula → Prop,
  (∀ a : Formula, (∀ b : Formula, lt_depth b a → P b ) → P a ) →
  ∀ a : Formula, P a.

Lemma Formula_depth_ind2 :
∀ P : Formula → Prop,
(∀ t t0 : Term, P (equal t t0)) →
(∀ (r : Relations L)
         (t : Terms (arityR L r)),
     P (atomic r t)) →
(∀ f : Formula, P f → ∀ f0 : Formula, P f0 → P (impH f f0)) →
(∀ f : Formula, P f → P (notH f)) →
(∀ (v : nat) (a : Formula),
  (∀ b : Formula, lt_depth b (forallH v a) → P b ) → P (forallH v a)) →
∀ f : Formula, P f.

End Formula_Depth_Induction.

End First_Order_Logic.

Implicit arguments and notations

In Russel O'Connor's work, the abstract syntax of first-order terms and formulas is available in three versions:

A generic one (for any Language L)
An instantiation for the language of number theory LNT
An instantiation for the language of natural numbers LNN

In the current version, we propose to use three notation scopes: fol_scope, nt_scope and nn_scope, in order to make clear the relationship between the three sets of formulas.

fol_scope is defined in this file, lnt_scope in LNT.v, and lnn_scope in LNN.v,

Implicit arguments

The original code of this library contains some redefinitions like

Definition Formula := Formula LNN.

We plan to use systematically implicit arguments and avoid such redefinitions, which make more complex formula and term displaying, e.g. in goals or results of computation.

Arguments impH {L} _ _.
Arguments notH {L} _.
Arguments forallH {L} _ _.
Arguments orH {L} _ _.
Arguments andH {L} _ _.
Arguments iffH {L} _ _.
Arguments equal {L} _ _.
Arguments existH {L} _ _.
Arguments var {L} _.
Arguments atomic {L} _ _.
Arguments apply {L} _ _.
Arguments ifThenElseH {L} _ _ _.
Arguments Tnil {L}.
Arguments Tcons {L} {n} _ _.

Notation "'f[' A ']f'" := A (A custom fol at level 200).

Notation "x ∨ y" := (orH x y) (in custom fol at level 85, x custom fol, y custom fol, right associativity).

Notation "x ∧ y" := (andH x y) (in custom fol at level 80, x custom fol, y custom fol, right associativity).

Notation "x -> y" := (impH x y) (in custom fol at level 99, right associativity, y at level 200).

Notation "x <-> y" := (iffH x y) (in custom fol at level 99, right associativity, y at level 200).

Notation "~ x" := (notH x) (in custom fol at level 75, right associativity).

Notation "( x )" := x (in custom fol, x custom fol at level 200).

Notation "x = y" := (equal x y) (in custom fol at level 70, no associativity).

Notation "x <> y" := (notH (equal x y)) (in custom fol at level 70, no associativity).

Notation "{ x }" := x (in custom fol, x constr).

Notation "'∀' i ',' f" := (forallH i f) (in custom fol at level 200, i constr, f custom fol at level 200).

Notation "'∃' i , f" := (existH i f)
(in custom fol at level 200, i constr, f custom fol at level 200).

Check f [ ∀ 3, ∃ 4, {equal (var 3) (var 4)} ∨ {var 3} = {var 4} ]f.

Check f [ ¬ { equal (var 3) (var 4) } ]f.

Check f [ {var 3} ≠ {var 4} ]f.

Check f [ ¬ ( {var 3} = {var 4} ) ]f.

The fol_scope notation scope

Module FolNotations.
Declare Scope fol_scope.
Delimit Scope fol_scope with fol.

Infix "=" := (equal _): fol_scope.
Infix "∨" := (orH): fol_scope.
Infix "∧" := (andH):fol_scope.
Infix "→" := (impH): fol_scope.
Notation "~ A" := (@notH _ A): fol_scope.
Notation "A <-> B" := (@iffH _ A B): fol_scope.

Notation "'v#' i" := (var i) (at level 3, format "'v#' i", i at level 0) : fol_scope.
Notation "'exH' x .. y , p" := (existH x .. (existH y p) ..)
(x at level 0, y at level 0, at level 200, right associativity) : fol_scope.
Notation "'allH' x .. y , p" := (forallH x .. (forallH y p) ..)
(x at level 0, y at level 0, at level 200, right associativity) : fol_scope.

Notation "t = u" := (@equal _ t u): fol_scope.
Notation "t <> u" := (¬ t = u)%fol : fol_scope.

the following notations are used when some computation expands a disjunction, conjuction, etc. in terms of implication and negation

Reserved Notation "x '\/'' y" (at level 85, right associativity).
Reserved Notation "x '/\'' y" (at level 80, right associativity).
Reserved Notation "x '<->'' y" (at level 95, no associativity).
Reserved Notation "x '<->''' y" (at level 95, no associativity).

Notation "x \/' y" := (¬ x → y)%fol : fol_scope.
Notation "x /\' y" := (¬ (~ x \/' ¬ y))%fol : fol_scope.
Notation "x <->'' y" := ((x → y) ∧ (y → x))%fol: fol_scope.
Notation "x <->' y" := (¬ (~ (x → y) \/' ¬ (y → x)))%fol : fol_scope.
Notation exH' v A := (¬ (forallH v (¬ A)))%fol.

End FolNotations.

Import FolNotations.
Check (v #5)%fol.

Examples

Section LExamples.
Variable L: Language.
Variables P Q : Formula L.

Let ex1 : Formula L := (P ∧ Q)%fol.

Let ex2 : Formula L := (¬ (~ ¬P → ¬Q ))%fol.

Let ex3 : Formula L:= (¬ (~P ∨ ¬Q ))%fol.

End LExamples.

Section Correctness.
Variable L: Language.
Variables P Q R : Formula L.

Goal (P ∨ Q )%fol = (P \/' Q )%fol.

Goal (P ∧ Q )%fol = (P /\' Q )%fol.

End Correctness.