Does `p → p` require `open Classical`?

Stream: new members

[Lars Ericson]

I have in mind that p → q is shorthand for ¬p ∨ q in which case p → p is really p ∨ ¬p which is em. Is that correct, or am I missing a subtlety?

[Richard Copley]

In systems based on type theory, function types such as p → q are fundamental. The honest answer to your question is "no". One could write quite a long essay on this, but perhaps here is not the place (and certainly I'm not the right person). Such essays must already exist, if you can find some introductory material on type theory in logic.

[Eric Wieser]

Another way of explaining your remark: your use of the word "shorthand" or "is really" is a) not the "definitional equality" meaning of "is" that type theory cares about and b) invoking em to justify the equality

[Lars Ericson]

I am looking at this exercise, which should not require Classical, but where I need to show p → p to finish it. Based on my old understanding that p → p was shorthand for ¬p ∨ p , I was unsure what to do next. I am unsure whether (intuitonistic?) type theory gives me p → p as an axiom or otherwise without resorting to open Classical:

example : p ∨ False ↔ p :=
  have fwd : p ∨ False → p  :=
    fun hpf : p ∨ False =>
      have hpf1 : p → p := sorry -- em?
      Or.elim hpf hpf1 False.elim
  Iff.intro fwd Or.inl

[Eric Wieser]

Maybe it helps to think how you would "prove" Nat → Nat

[Matt Diamond]

Implications are just functions, so a proof of p implies q is just a function that takes a proof of p and returns a proof of q

[Lars Ericson]

OK

theorem pp: p → p :=
  fun hp : p =>
    hp

[Matt Diamond]

Looks good! id should work as well

[Lars Ericson]

Of course

example : p ∨ False ↔ p :=
  have pp : p → p := fun hp: p => hp
  have fwd : p ∨ False → p  :=
    fun hpf : p ∨ False =>
      Or.elim hpf pp False.elim
  Iff.intro fwd Or.inl

then remembering id

example : p ∨ False ↔ p :=
  have fwd : p ∨ False → p  :=
    fun hpf : p ∨ False =>
      Or.elim hpf id False.elim
  Iff.intro fwd Or.inl

Trying to figure out what is classical and what isn't puts me in deer-in-the-headlights state sometimes.

[Mario Carneiro]

I should really port itauto...

[Eric Wieser]

How usable will https://github.com/leanprover-community/mathlib3port/blob/4e6c8360770e7f9aba55a7c32040065de4f9d823/Mathbin/Tactic/Itauto.lean be?

[Mario Carneiro]

what do you mean? It was designed for the kind of problems lars is asking

[Mario Carneiro]

in particular, it generates really nice proofs that can be viewed in #explode, a property definitely not shared with tauto, simp, decide or other similar ways of proving this

[Mario Carneiro]

well, simp will create okayish proofs but mainly because all of these things are already theorems

[Mario Carneiro]

and it will also wrap it in a bunch of junk with congrFun and iff_true and propext

[Mario Carneiro]

Oh I realize now that you are asking whether the mathlib3port output will be useful for doing the port, and the answer is that it is rarely all that useful for meta code, in part because we didn't set up even basic mappings like expr -> Lean.Expr. But it's possible to read the code and manually translate without too much difficulty

[Mario Carneiro]

Actually it's not that bad, because unlike many tactics itauto is 90% pure code, one could even prove the core function correct if desired, and only the reification part needs a rewrite

[Lars Ericson]

@Richard Copley instead of writing a long essay, would be possible to prove, in the absence of open Classical, that

theorem pp_isnt_em : ¬ ((p → p) ↔ (¬p ∨ p)) :=
  sorry

or is there something meta about this that eludes proof? Or is it hard to phrase and I haven't phrased it correctly with pp_isnt_em?

That said, I have finished the non-Classical exercises in the book, with liberal use of haves and no lemmas. This was good exercise, I have developed some muscle memory for False.elim, Or.elim, And.intro, Or.inr, Or.inl and Iff.intro to the extent that applying these feels mechanical. I only had to open Mathlib for imp_false.2, but that was only after I proved imp_false.2 on my own and then went looking for it in Mathlib, since it looked fundamental:

import Std.Logic

example : (p → (q → r)) ↔ (p ∧ q → r) :=
  have fwd : (p → (q → r)) → (p ∧ q → r) :=
    fun hpqr : p → q → r =>
      fun hpq : p ∧ q =>
        have hp : p := hpq.left
        have hq : q := hpq.right
        hpqr hp hq
  have back : (p ∧ q → r) → (p → (q → r)) :=
    fun hpqr : (p ∧ q → r) =>
      fun hp : p =>
        fun hq : q =>
          have hpq : p ∧ q := ⟨ hp, hq ⟩
          hpqr hpq
  Iff.intro fwd back

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
  have fwd : ((p ∨ q) → r) → (p → r) ∧ (q → r) :=
    fun hpqr : (p ∨ q) → r =>
      have hpr : p → r :=
        fun hp : p =>
          have hpq : p ∨ q := Or.inl hp
          hpqr hpq
      have hqr : q → r :=
        fun hq : q =>
          have hpq : p ∨ q := Or.inr hq
          hpqr hpq
      And.intro hpr hqr
  have back : (p → r) ∧ (q → r) → ((p ∨ q) → r) :=
    fun hprqr : (p → r) ∧ (q → r) =>
      have hpr : p → r := hprqr.left
      have hqr : q → r := hprqr.right
      fun hpq: p ∨ q =>
        Or.elim hpq hpr hqr
  Iff.intro fwd back

example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
  have fwd : ¬(p ∨ q)  → ¬p ∧ ¬q  :=
    fun hnpq : ¬(p ∨ q) =>
      have hnp : ¬p :=
        fun hp : p =>
          have hpq : p ∨ q := Or.inl hp
          hnpq hpq
      have hnq : ¬q :=
        fun hq : q =>
          have hpq : p ∨ q := Or.inr hq
          hnpq hpq
      And.intro hnp hnq
  have back : ¬p ∧ ¬q → ¬(p ∨ q)  :=
    fun hnpnq : ¬p ∧ ¬q =>
      have hnp : ¬p := hnpnq.left
      have hnq : ¬q := hnpnq.right
      fun hpq : p ∨ q =>
        have hpf : p → False := imp_false.2 hnp
        have hqf : q → False := imp_false.2 hnq
        Or.elim hpq hpf hqf
  Iff.intro fwd back

example : ¬p ∨ ¬q → ¬(p ∧ q) :=
  have cnp : ¬p → ¬(p ∧ q) :=
    fun hnp : ¬p =>
      fun hpq : p ∧ q =>
        have hp : p := hpq.left
        hnp hp
  have cnq : ¬q → ¬(p ∧ q) :=
    fun hnq : ¬q =>
      fun hpq : p ∧ q =>
        have hq : q := hpq.right
        hnq hq
  fun hpq : ¬p ∨ ¬q =>
    Or.elim hpq cnp cnq

example : ¬(p ∧ ¬p) :=
  fun hpp : (p ∧ ¬p) =>
    have hp : p := hpp.left
    have hnp : ¬p := hpp.right
    have hF : False := hnp hp
    hF

example : p ∧ ¬q → ¬(p → q) :=
  fun hpq : p ∧ ¬q =>
    have hp : p := hpq.left
    have hnq : ¬q := hpq.right
    fun hpq : p → q =>
      have hq : q := hpq hp
      hnq hq

example : ¬p → (p → q) :=
  fun hnp : ¬p =>
    fun hp : p =>
      absurd hp hnp

example : (¬p ∨ q) → (p → q) :=
  fun hpq : (¬p ∨ q) =>
    fun hp : p =>
      have hnpq : ¬p → q :=
        fun hnp : ¬p =>
          absurd hp hnp
      Or.elim hpq hnpq id

example : p ∨ False ↔ p :=
  have fwd : p ∨ False → p  :=
    fun hpf : p ∨ False =>
      Or.elim hpf id False.elim
  Iff.intro fwd Or.inl

example : p ∧ False ↔ False :=
  have fwd : p ∧ False → False  :=
    fun hpf : p ∧ False =>
      hpf.right
  have back : False → p ∧ False :=
    fun hf : False =>
      False.elim hf
  Iff.intro fwd back

theorem foo  (hpq : p → q) (hnq : ¬q) : ¬p :=
  fun hp : p =>
    have hq : q := hpq hp
    absurd hq hnq

example : (p → q) → (¬q → ¬p) :=
  fun hpq : p → q =>
    fun hnq : ¬q =>
      fun hp : p =>
          have hq : q := hpq hp
          absurd hq hnq

[Richard Copley]

Usually in order to show that a result is non-classical nonconstructive one proves (constructively) that it is equivalent to a result that is known to be nonconstructive. That's not a very satisfying answer (since it's em itself that we want to show is nonconstructive, so my answer there just says "because it is"), but it's the best I know.

[Lars Ericson]

@ZHAO Jiecheng, in light of @Richard Copley's observations above, what are your thoughts on

-- "open Classical " not allowed for this exercise

example : ¬ ((p → p) ↔ (¬p ∨ p)) :=
  sorry

[ZHAO Jiecheng]

Sorry, but I feel there must be something wrong with your settings. It is really unusual that you write this kind of proof. Are you using vscode or nvim or other supported editors and are all the plugins installed correctly.

[ZHAO Jiecheng]

This is my proof of example : ¬(p ∨ q) ↔ ¬p ∧ ¬q the editor plugin will hint you the type of each term you should fill. There is no need to write down and make these things with have by your own. You can write the code just like in a tactic model. Writing so many have in your code may indicate that you do not use the help of the editor which will make everything much harder.

Screencast-from-2024年01月02日-10时52分09秒.webm

example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
  have fwd : ¬(p ∨ q)  → ¬p ∧ ¬q  :=
    fun hnpq : ¬(p ∨ q) =>
      have hnp : ¬p :=
        fun hp : p =>
          have hpq : p ∨ q := Or.inl hp
          hnpq hpq
      have hnq : ¬q :=
        fun hq : q =>
          have hpq : p ∨ q := Or.inr hq
          hnpq hpq
      And.intro hnp hnq
  have back : ¬p ∧ ¬q → ¬(p ∨ q)  :=
    fun hnpnq : ¬p ∧ ¬q =>
      have hnp : ¬p := hnpnq.left
      have hnq : ¬q := hnpnq.right
      fun hpq : p ∨ q =>
        have hpf : p → False := imp_false.2 hnp
        have hqf : q → False := imp_false.2 hnq
        Or.elim hpq hpf hqf
  Iff.intro fwd back

example : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
  Iff.intro
    (
      fun h : ¬(p ∨ q) => ⟨
      (fun hp: p => h (Or.inl hp)),
      (fun hq: q => h (Or.inr hq))⟩
    )
    (
      fun h: ¬p ∧ ¬q => fun hpq: p ∨ q =>
        hpq.elim
        (fun hp: p => h.left hp)
        (fun hq: q => h.right hq)
    )

[Lars Ericson]

@ZHAO Jiecheng I was moving the context of your reply in this other thread here to relate to my ongoing reading of the Theorem Proving text. I completed the non-Classical exercises in this section. The problem above occurred to me in asking for help on the non-Classical examples. The question is not a result of assistance from vscode or nvim. I am using the Lean 4 playground on the web to edit my examples. The question is about an equivalence that is typically learned in a basic logic class but which does not hold in the type theory approach used by Lean. This equivalence doesn't hold in the Lean setting. It seems interesting to ask how it would be formally described or established. The question is outside of the book and has nothing to do with text editors.

[Lars Ericson]

The statement is that in Lean, p → p is not the same as ¬p ∨ p. This goes to the old-school logic equivalence of p → q and ¬p ∨ q. Please read the answers above to understand the particular question I am asking.

[Richard Copley]

One I prepared earlier (not different from your second proof, @ZHAO Jiecheng, but golfed)

example : ¬(p ∨ q) ↔ (¬p ∧ ¬q) := ⟨
  fun h => ⟨fun hp => h (Or.inl hp), fun hq => h (Or.inr hq)⟩,
  fun h₁ h₂ => h₂.elim h₁.left h₁.right⟩

[Richard Copley]

@Lars Ericson, p → p is provable, as you know, so the remaining part of your challenge is, "Either prove that ¬p ∨ p, or prove that ¬(¬p ∨ p)."
You will not be able to do either of those. As for proving that it is not possible: I think you need some model theory. It's a little further than I every really got with logic. But not too much further. I am certain there are books that are not too hard that cover this in detail.

[Mario Carneiro]

Incidentally, itauto (which I am currently rescuscitating) will be able to solve questions of the form "is this intuitionistically provable", because it is complete for intuitionistic propositional logic

[ZHAO Jiecheng]

@Lars Ericson You can not prove this. You can never prove a false without AC when you can prove a true with AC. For (p → p) ↔ (¬p ∨ p)is true with AC you can never prove ¬ ((p → p) ↔ (¬p ∨ p)) without AC.

Or it means you can prove False after AC added.

open Classical
example (h: ¬((p → p) ↔ (p ∨ ¬p))): False :=
  h ⟨fun _ => em p, fun _ => id⟩

[ZHAO Jiecheng]

Mario Carneiro said:

Incidentally, itauto (which I am currently rescuscitating) will be able to solve questions of the form "is this intuitionistically provable", because it is complete for intuitionistic propositional logic

Out of curiosity, how it can be complete without EM. Is there any reference for paper?

[llllvvuu]

p → q is shorthand for ¬p ∨ q

I'm not sure this is true in classical propositional calculus either since this is a "rule of inference" rather than how implication is defined (implication is its own fundamental concept).

And in Lean, (p → q) => ¬p ∨ q is a theorem (docs#Decidable.not_or_of_imp) depending on em (via docs#Classical.propDecidable):

FWIW in intuitionistic logic, the rule of inference is (p → q) => ¬(p ∧ ¬q). This you can actually write as a program:

def imp_example {p q : Prop} (h : p → q) :
    (And p (q → False)) → False :=
  fun ⟨ hp, hq ⟩ => hq (h hp)
#print axioms imp_example

(if you'd rather come at it from the angle of a programmer rather than a logician)

[Mario Carneiro]

ZHAO Jiecheng said:

Mario Carneiro said:

Incidentally, itauto (which I am currently rescuscitating) will be able to solve questions of the form "is this intuitionistically provable", because it is complete for intuitionistic propositional logic

Out of curiosity, how it can be complete without EM. Is there any reference for paper?

I said "complete for intuitionistic logic". That means that if there exists a proof without EM, then itauto will find it, and contrapositively if it reports failure then no proof exists and there is a countermodel (which will be some kind of Kripke frame). It is based on the G4ip algorithm from Contraction-free sequent calculi for intuitionistic logic

[Mario Carneiro]

On my itauto branch:

example : (p → p) ↔ (¬p ∨ p) := by itauto! [p]
example : (p → p) ↔ (¬p ∨ p) := by itauto -- failed

[ZHAO Jiecheng]

Mario Carneiro said:

On my itauto branch:

example : (p → p) ↔ (¬p ∨ p) := by itauto! [p]
example : (p → p) ↔ (¬p ∨ p) := by itauto -- failed

And branch on Github to have a quick access?

[Mario Carneiro]

#9398

[Lars Ericson]

Lean 4, with its hierarchy of universes, has a flexibility that may allow for constructing more metamathematical arguments than a system without a hierarchy of universes. If model theory is required, perhaps proofs in model theory could be formalized in Lean.

Please let me rephrase my question: Let L be a system of logic with axioms A₁,A₂,...,An. If a proposition P↔Q depends on axiom Ai to prove, andAi is removed, how do you show, verifiably, that no proof exists in L-Aiof P↔Q? To simplify, suppose that Ai=P↔Q.

In other words, say that there is nothing in {A₁,A₂,...,An}\{Ai} which contradicts Ai. In that case, other than just saying "Well, it's not there!", how do you show that Ai is not provable in L-Ai?

If this were a vector space question, it would amount to proving that A₁,A₂,...,An is a set of mutually orthogonal basis vectors, and from there show that, by virtue of being mutually orthogonal, you can't "add up" any of the Aj, j≠i, to get Ai. Along those lines, how would you show, mechanically verifiably, that a particular set of axioms are mutually orthogonal, say in some kind of space of proofs?

[Mario Carneiro]

The vector space analogy is reasonably good. Proofs are linear combinations of basis vectors, and countermodels are proper subspaces which contain all the specified basis vectors

[Mario Carneiro]

The way you construct a model for a theory is the same way as you do any other kind of abstract algebra, you construct a set satisfying a bunch of properties

[Mario Carneiro]

in fact most abstract algebraic classes are models of specific first order axiom systems. For example groups are just models of first order logic with equality, a binary function symbol * and some axioms about it

[Mario Carneiro]

if you want to prove AC is independent of ZF, you construct a model of ZF where AC is false and a model of ZF where AC is true

[Mario Carneiro]

You can prove that the axiom \forall x, \exists y, x * y = 1 is independent of the monoid axioms, because there exist monoids that are not groups. So the proof is "Observe: Nat is an additive monoid, and it is not an additive group. QED"

[Lars Ericson]

Thanks @Mario Carneiro for that example.

Here is a discussion from Noah Schweber on this example..

Even better, here is a Bachelor's thesis by Elliot Belbin going through the proof of the independence of the axiom of choice in set theory. Do you think it would be possible to express and check the model-theoretic constructions and theorems in this thesis in Lean 4? That would be a fun project.

[Lars Ericson]

Also following on the mutual orthogonality idea, another version of that is to show a dimension reduction, e.g. if I have i = (1,0,0), j = (0,1,0) and k = (0,0,1), then I can express points in 3 dimensions. If I take away k, then I can "compress" i and j to be i = (1,0) and j = (0,1) and effect a dimension reduction. So if you can show that taking away em from the axioms of Lean 4 results in a dimension reduction, that seems like a slightly different avenue of proof than proving that the axioms are mutually orthogonal (although it may be saying the same thing).

[Lars Ericson]

P.S. I guess the answer is yes.

[Mario Carneiro]

well, that one is about the independence of CH from ZFC, so independence of AC from ZF is still an available project... I believe the proofs have a lot of commonality

[Lars Ericson]

So:

• Flypitch is independence of CH from ZFC: formally verified in Lean, blazing a trail.
• Belbin (attached) is independence of AC from ZF. I will put verification of Belbin's thesis on my Lean bucket list, just after actually learning Lean thoroughly through all my bookmarked texts.
• Regarding independence of EM from intuitionistic logic, I could only find this Stack Exchange post. Other than that, ChatGPT/Bard/BingChat can cite no article which gives the proof. I didn't find anything in Google Scholar. This is quite surprising, given how plowed under and relatively old the topic is, and what low-hanging fruit this would seem to be. If there is no complete writeup, would writing out and formally verifying this proof qualify as a PhD thesis in Math? MS Thesis? Or just Bachelor's thesis, like AC from ZF?

[Mario Carneiro]

They teach that one in school (if you take the right classes). The two main proofs are the topological one (https://math.stackexchange.com/a/1371237/50776) and the one with a two element kripke frame (https://math.stackexchange.com/a/2888061/50776)

[Joseph Myers]

Mathlib already has Heyting algebras; constructing a suitable instance and showing it doesn't satisfy EM would surely be both straightforward and appropriate for Counterexamples/ (if not mathlib proper).