Code Review: Proving that a simple propositional logic satisfies Aristotle's Thesis

Question

I'm proving that a simple propositional logic satisfies Aristotle's thesis.

I'm curious how to improve the code in question.

Here are the things I know that are wrong with it:

• I'm using nat as the set of variables. I'm not sure how to fix this. I at first tried making OpenWff depend on a parameter V : Set but that's not right. We don't have a well-formed formula for every possible set of variables.
• I'm representing an environment as env : nat -> TruthValue. In order to prove a statement for all environments, I instead iterated over all truth values and looked at constant environments in a lemma called AristotleImpl. I'm curious if there's a better strategy that works here.

And here's what I'm trying to do next:

• Figure out how to state and prove that substitution instances of true well-formed formulas are true.

---

Context: Connexive Logics And Logics With Separate Truth and Falsity Conditions

---

I'm investigating a simple connexive logic. For some background on connexive logics, see this video.

In particular, I'm looking at some interesting ways of defining a logical system that satisfies Aristotle's thesis (shown below).

$$ A \to \lnot A \;\; \textit{never has a designated truth value} \;\; \text{is Aristotle's thesis} $$

Hitoshi Omori remarks at around 18m39s that intepreting $\to$ as the classical biconditional works and is the simplest possible connexive logic. This remark is mostly intended to show that adding a few axioms to a KD-like system results in a collapse of sorts, and $\to$ being biconditional-like is a fate that we want to avoid.

In that presentation and also in this paper there are quite a few systems that are defined by giving separate truth and falsity conditions.

I had an idea a few days ago to do something kind of similar and look at truth conditions and formula complexity. Formula complexity being a thing that we get to define as builders of the system (similar to falsity conditions) that's inspired by a concept that's normally primitive (the length of a formula (or a formula not being true in the case of falsity conditions)). I'm looking at a couple of different choices for how to define formula complexity (such as only counting binary connectives) and how to use $<,\le,=, \neq$ comparisons in the truth conditions of formulas, I'm just picking an easy one here to formalize in Coq as a starting point.

Every well-formed formula $\varphi$ is true or not true. Additionally, every well-formed formula has a complexity, denoted $|\varphi|$, which is inspired by the number of connectives that a well-formed formula contains.

Suppose I have the connectives $\lnot$ and $\to$.

If $\alpha$ is a primitive variable, then $\alpha$ is true if and only if $\alpha$ is true in the current context.

$\lnot \alpha$ is true if and only if $\alpha$ is not true.

$\alpha \to \beta$ is true if and only if ($\alpha$ is true iff $\beta$ is true) or ($\alpha$ is not true and $\alpha$ and $\beta$ have the same complexity).

If $\alpha$ is a primitive variable, $|\alpha|$ is the complexity of $\alpha$ in the current context.

$|\lnot \alpha|$ is equal to $1+|\alpha|$.

$|\alpha \to \beta|$ is equal to $1+|\alpha|+|\beta|$.

So, $A \to \lnot A$ is clearly a contradiction because $A$ and $\lnot A$ will never have the same length and will never have the same truth value.

---

Here's the code. Its biggest problem probably is the use of nat as the wff's rather than a more appropriate type.

Require Import Arith.


Record TruthValue : Type :=
  { truth : Prop
  ; complexity : nat
  }.


Inductive OpenWff : Type :=
| Var : nat -> OpenWff
| Not : OpenWff -> OpenWff
| Imp : OpenWff -> OpenWff -> OpenWff.


Fixpoint Complexity (wff: OpenWff) (env : nat -> TruthValue) : nat :=
  match wff with
  | Var v => complexity (env v)
  | Not wff' => 1 + Complexity wff' env
  | Imp a b => 1 + (Complexity a env) + (Complexity b env)
  end.

Fixpoint Truth (wff : OpenWff) (env : nat -> TruthValue) : Prop :=
  match wff with
  | Var v => truth (env v)
  | Not wff' => not (Truth wff' env)
  | Imp a b => (
                ((Truth a env) <-> (Truth b env)) \/
                  ((not (Truth a env)) /\ Complexity a env = Complexity b env )
              )
  end.

Lemma AristotleImpl : forall tv : TruthValue,  not (Truth (Imp (Var 0) (Not (Var 0))) (fun x => tv)).
Proof.
  intros.
  unfold Truth.
  intuition.
  induction tv.
  unfold Complexity in H1.
  simpl in H.
  simpl in H1.
  induction complexity0.
  discriminate.
  intuition.
  Qed.


Theorem Aristotle : forall env : nat -> TruthValue, not (Truth (Imp (Var 0) (Not (Var 0))) env).
Proof.
  intros.
  apply AristotleImpl.
Qed.

Answer 1

Here is how you can defer the choice of what variables are to a later time. This amounts to making OpenWff depend on a parameter; I'm not sure why that was giving you trouble.

I also switched the order of the arguments so that env appears before the formula, because intuitively to me you will more often want to fix the env than the formula. If this is not the case, feel free to switch it back.

Section Aristotle.

Variable V : Type.

Record TruthValue : Type :=
  { truth : Prop
  ; complexity : nat
  }.

Inductive OpenWff : Type :=
| Var : V -> OpenWff
| Not : OpenWff -> OpenWff
| Imp : OpenWff -> OpenWff -> OpenWff.


Fixpoint Complexity (env : V -> TruthValue) (wff : OpenWff) : nat :=
  match wff with
  | Var v => complexity (env v)
  | Not wff' => 1 + Complexity env wff'
  | Imp a b => 1 + (Complexity env a) + (Complexity env b)
  end.

Fixpoint Truth (env : V -> TruthValue) (wff : OpenWff) : Prop :=
  match wff with
  | Var v => truth (env v)
  | Not wff' => not (Truth env wff')
  | Imp a b => (
                ((Truth env a) <-> (Truth env b)) \/
                  ((not (Truth env a)) /\ Complexity env a = Complexity env b)
               )
  end.

Lemma AristotleImpl : forall (xv : V) (tv : TruthValue),
  not (Truth (fun x => tv) (Imp (Var xv) (Not (Var xv)))).
Proof.
  intros.
  unfold Truth.
  intuition.
  induction tv.
  unfold Complexity in H1.
  simpl in H.
  simpl in H1.
  induction complexity0.
  - discriminate.
  - intuition.
Qed.

Theorem Aristotle : forall (env : V -> TruthValue) (xv : V),
  not (Truth env (Imp (Var xv) (Not (Var xv)))).
Proof.
  intros.
  apply (AristotleImpl xv).
Qed.

End Aristotle.

I have used a Section, but this could also be done without it. Note that outside the section the variable V will be quantified everywhere it appears. For example:

Print OpenWff.
(*
Inductive OpenWff (V : Type) : Type :=
    Var : V -> OpenWff V
  | Not : OpenWff V -> OpenWff V
  | Imp : OpenWff V -> OpenWff V -> OpenWff V.
*)

Note also that I needed to quantify over xv : V in the lemmas instead of using 0 as a kind of default.

---

Here is how you can prove your theorem without the auxiliar lemma:

Theorem Aristotle : forall (env : V -> TruthValue) (xv : V),
  not (Truth env (Imp (Var xv) (Not (Var xv)))).
Proof.
  intros env xv; simpl.
  case (env xv); simpl.
  intros tr comp [equiv_tr_ntr|[_ eq_comp_Scomp]].
  - intuition.
  - apply (n_Sn _ eq_comp_Scomp).
Qed.

The key insight is that you can destruct env xv directly, there's no need to have a variable tv : TruthValue.

---

Figure out how to state and prove that substitution instances of true well-formed formulas are true.

The first thing to note is that if you want to speak about replacing a variable by another, you will need a (decidable) way to compare variables:

Variable eqV : V -> V -> bool.

This will represent equality in V, and you may need to assume further properties about it, such as reflexivity, symmetry, and transitivity.

After you have decidable equality, you can define substitution as follows:

(* replace x by y *)
Fixpoint sub (wff : OpenWff) (x y : V) : OpenWff :=
  match wff with
  | Var z => if eqV x z then Var y else Var x
  | Not wff' => Not (sub wff' x y)
  | Imp a b => Imp (sub a x y) (sub b x y)
  end.

Then my understanding of what you want to prove could be stated as

Theorem sub_Truth (wff : OpenWff) (x y : V) :
  (forall env, Truth env wff) -> (forall env, Truth env (sub wff x y)).

In order to prove this theorem you will need to be able to manipulate an env in order to turn it into another env with some desirable properties. For example, the following definition ought to be useful:

Definition sub_env (env : V -> TruthValue) (x : V) (px : TruthValue) := fun z =>
  if eqV x z then px else env z.

You'll also want to prove a lemma about how sub and sub_env interact, another on how sub and Complexity interact, and probably some others. (I haven't actually proved this theorem.)