1階論理

1階（古典）論理を扱う。

Require Import finite_sequence.

Set Implicit Arguments.

Definition variable : Type := nat.

Record signature : Type :=
  make_signature {
    fn_sym : nat -> Type;
    pr_sym : nat -> Type;
  }.

Section Syntax.
  Variable L : signature.

  Inductive term : Type :=
    | Var : variable -> term

    | FnSym {a} (f : L.(fn_sym) a)
      : fin_seq term a -> term.

  Inductive formula : Type :=
    | PrSym {a} (p : L.(pr_sym) a)
      : fin_seq term a -> formula

    | Or  : formula -> formula -> formula
    | Neg : formula -> formula
    | Ex  : formula -> formula
    | Eq  : term -> term -> formula.

  Definition And
    (A B : formula)
    : formula :=
    Neg (Or (Neg A) (Neg B)).

  Definition All
    (A : formula)
    : formula :=
    Neg (Ex (Neg A)).

  Definition NEq
    (M N : term)
    : formula :=
    Neg (Eq M N).
End Syntax.

Record theory : Type :=
  make_theory {
    L        :> signature;
    is_axiom : formula L -> Prop;
  }.

Section Logic.
  Variable T : theory.

  Inductive axiom : formula T.(L) -> Prop :=
    | LEM A : axiom (Or A (Neg A))
    | Id  M : axiom (Eq M M)
    .

  Inductive rule : formula T.(L) -> formula T.(L) -> Prop :=
    | Expansion A B : rule A (Or B A)
    | Contr A       : rule (Or A A) A
    | Assoc A B C   : rule (Or (Or A B) C) (Or A (Or B C))
    .
End Logic.

ShoenfieldのMathematical LogicにおけるN:

Inductive arithmetic_fn_sym : nat -> Type :=
  | Zero : arithmetic_fn_sym 0
  | Suc  : arithmetic_fn_sym 1
  | Add  : arithmetic_fn_sym 2
  | Mul  : arithmetic_fn_sym 2.

Inductive arithmetic_pr_sym : nat -> Type :=
  | LessThan : arithmetic_pr_sym 2.

Definition arithmetic_signature : signature :=
  make_signature
    arithmetic_fn_sym
    arithmetic_pr_sym.

Abbreviation zero := (FnSym (L := arithmetic_signature) Zero nil).

Abbreviation suc M := (FnSym (L := arithmetic_signature) Suc (cons M nil)).

Inductive arithmetic_axiom : (formula arithmetic_signature) -> Prop :=
  | Ax1 : arithmetic_axiom (NEq (suc (Var arithmetic_signature O)) zero)
  .

Definition arithmetic_theory : theory :=
  make_theory
    arithmetic_axiom.