reinterpret ax-3

[ookami]

Hello,

After all the years I now improve && extend in particular the propositional logic section,

I am still stuck with a fundamental question.

Is there a good reason why negation is handled differently from the bi-conditional?

The definition of <-> is implicit. We learn that it must obey a particular expression, that

enables us to retrieve the characteristics of this operator later.

Why on earth is the same not done with negation? One can easily reinterpret axiom ax-3

as an implicit *definition* of negation, thus mandating a renaming to df-neg. The

characteristics of negation are then determined likewise.

Is it more difficult to arrive at something like bijust?

Looking forward to answers.

Wolf Lammen

[Mario Carneiro]

It's not a conservative extension, as the intuitionistic logic development makes clear. Peirce's law ((p -> q) -> p) -> p is not provable from ax-1,2,mp but it is provable from ax-1,2,3,mp, even though there are no negations involved in the statement. By contrast, df-bi is a conservative extension even though it has a peculiar form. This is easy to prove because you can replace (p <-> q) with -. ((p -> q) -> -. (q -> p)) everywhere in a proof using biconditionals to reduce it to a proof which refers to the theorem bijust instead of df-bi, in the original axiom system.

On Sun, Mar 8, 2020 at 4:44 AM 'ookami' via Metamath <meta...@googlegroups.com> wrote:

Hello,

After all the years I now improve && extend in particular the propositional logic section, I am still stuck with a fundamental question.

Is there a good reason why negation is handled differently from the bi-conditional? The definition of <-> is implicit. We learn that it must obey a particular expression, that enables us to retrieve the characteristics of this operator later.

Why on earth is tjhe same not done with negation? One can easily reinterpret axiom ax-3 as an implicit *definition* of negation, thus mandating a renaming to df-neg. The characteristics of negation are then determined likewise.

Looking forward to answers.

Wolf Lammen

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/42f13847-f827-4ce2-b39c-1528e5d76f40%40googlegroups.com.

[ookami]

Am Sonntag, 8. März 2020 14:06:25 UTC+1 schrieb Mario Carneiro:

It's not a conservative extension, as the intuitionistic logic development makes clear. Peirce's law ((p -> q) -> p) -> p is not provable from ax-1,2,mp

There is some connection to theoretical computer science here, in particular grammars. I (faintly) remember,

that the richness of constructable strings, and decidability (is a particular string contructable) are prominent

questions in this part. It is way long back, that I dealt with questions like this. I still try to translate your

words to what I remember from courses then: conservative seems to mean fully decidable and all true

statements are reachable...

but it is provable from ax-1,2,3,mp, even though there are no negations involved in the statement. By contrast, df-bi is a conservative extension even though it has a peculiar form. This is easy to prove because you can replace (p <-> q) with -. ((p -> q) -> -. (q -> p)) everywhere in a proof using biconditionals to reduce it to a proof which refers to the theorem bijust instead of df-bi, in the original axiom system.

Thanks for your answer.

Wolf

[Benoit]

Sidenote: since bijust is a negation, it is provable from ax-mp, ax-1, ax-2, Peirce, and the minimalistic contraposition ( ( ph -> -. ps ) -> ( ps -> -. ph ) ).  This system is strictly weaker than classical propositional calculus, and is called "classical refutability".  So df-bi provides a definitional extension in this weaker system.

By contrast, bijust is (probably) not intuitionistic (one could try to find a counterexample using open subsets of \R, for instance, but this looks tedious; maybe Mario or Jim know a faster method), and this explains why df-bi is different in iset.mm.

Benoît

[Mario Carneiro]

If you actually want intuitionistic logic, you cannot get away with using just -> and -. as your basis. You have to add in /\ and \/ , but once you have that, you can just use dfbi1 as the definition (and df-bi is really just an obfuscated version of dfbi2 anyway, once you unfold the definition of /\ ).

Regarding provability of bijust, it is intuitionistically provable with the standard intuitionistic interpretations of -> and -. . It is an instance of -. ((p -> p) -> -. (p -> p)), which is true because |- p -> p is provable, and so from ((p -> p) -> -. (p -> p)) you can conclude -. (p -> p) and from there, falsity, so -. ((p -> p) -> -. (p -> p)).

--

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8bff49a5-66ea-4598-a0be-a156dcb02e32%40googlegroups.com.

[Mario Carneiro]

On Sun, Mar 8, 2020 at 9:18 PM Mario Carneiro <di....@gmail.com> wrote:

If you actually want intuitionistic logic, you cannot get away with using just -> and -. as your basis. You have to add in /\ and \/ , but once you have that, you can just use dfbi1 as the definition

correction: dfbi2

[Benoit]

> Regarding provability of bijust, it is intuitionistically provable with the standard intuitionistic interpretations of -> and -. . It is an instance of -. ((p -> p) -> -. (p -> p)), which is true because |- p -> p is provable, and so from ((p -> p) -> -. (p -> p)) you can conclude -. (p -> p) and from there, falsity, so -. ((p -> p) -> -. (p -> p)).

Of course !  Actually the current proof uses id, pm2.01 and mt2, which are all minimalistic.  I should have checked it first !  Therefore, set.mm's df-bi would provide a definitional extension in iset.mm as well, but it would define the "classical equivalence", which is strictly weaker than the intuitionistic equivalence.  Is that correct ?

> If you actually want intuitionistic logic, you cannot get away with using just -> and -. as your basis. You have to add in /\ and \/ , but once you have that, you can just use dfbi1 as the definition (and df-bi is really just an obfuscated version of dfbi2 anyway, once you unfold the definition of /\ ).

iset.mm's df-bi does not use \/ and seems to be conservative over the axioms for ->, -. and /\ alone, without the axiom for \/ ax-io.  Probably you mean in your first sentence the more general statement: *to achieve functional completeness*, you also need /\ and \/ ?

Benoît

[Mario Carneiro]

On Mon, Mar 9, 2020, 1:17 PM Benoit <benoit...@gmail.com> wrote:

> Regarding provability of bijust, it is intuitionistically provable with the standard intuitionistic interpretations of -> and -. . It is an instance of -. ((p -> p) -> -. (p -> p)), which is true because |- p -> p is provable, and so from ((p -> p) -> -. (p -> p)) you can conclude -. (p -> p) and from there, falsity, so -. ((p -> p) -> -. (p -> p)).

Of course !  Actually the current proof uses id, pm2.01 and mt2, which are all minimalistic.  I should have checked it first !  Therefore, set.mm's df-bi would provide a definitional extension in iset.mm as well, but it would define the "classical equivalence", which is strictly weaker than the intuitionistic equivalence.  Is that correct ?

Not quite. It is easy to see that classical equivalence is not equivalent to intuitionistic equivalence, for example (p <-> T.) is equivalent to p but (p <->c T.) is equivalent to -. -. p. But for this very reason, because df-bi shows only the classical equivalence of the newly defined notion to classical equivalence, it is not a definitional extension. I will show that df-bi is *also* provable if we interpret the new connective as intuitionistic equivalence! That is, ((p <-> q) <->c (p <->c q)) is provable in iset.mm.

It is not hard to show that (p <-> q) -> (p <->c q), so the goal reduces to -. -. ((p <->c q) -> (p <-> q)). Using the lemma (a -> -. -. b) -> -. -. (a -> b) this reduces to

((p <->c q) -> -. -. (p <-> q)) which is easy: unfolding the definition of <->c and applying contraposition it becomes

(-. (p <-> q) -> ((p -> q) -> -. (q -> p))), and after com12 and contraposition again becomes

((p -> q) -> ((q -> p) -> (p <-> q))) which is part of the definition of intuitionistic equivalence.

The lemma is not true in mimimal logic (or at least, the proof I will give makes essential use of ex falso). Suppose (1) (a -> -. -. b) and (2) -. (a -> b), we want to prove false. Applying (2) we have to show (a -> b) so suppose (3) a as well, we have to show b. By (1) and (3) we have -. -. b, and by (2) and (3) we have -. b, so false, so b by ex falso.

> If you actually want intuitionistic logic, you cannot get away with using just -> and -. as your basis. You have to add in /\ and \/ , but once you have that, you can just use dfbi1 as the definition (and df-bi is really just an obfuscated version of dfbi2 anyway, once you unfold the definition of /\ ).

iset.mm's df-bi does not use \/ and seems to be conservative over the axioms for ->, -. and /\ alone, without the axiom for \/ ax-io.  Probably you mean in your first sentence the more general statement: *to achieve functional completeness*, you also need /\ and \/ ?

Yes, that's what I meant. I'm mostly hedging because I don't usually consider "random subsets" of the logic by just cutting off certain axioms or connectives; I have decent intuitions for intuitionistic and minimal logic but for other subsets it becomes more delicate and I would have to work it out formally to say for sure.

Mario

[Benoit]

> That is, ((p <-> q) <->c (p <->c q)) is provable in iset.mm.

> [...] Using the lemma (a -> -. -. b) -> -. -. (a -> b)

Thanks.  So these two statements are intuitionistic.  They also hold in classical-refutability logic (simply because they are classical tautologies which remain classical tautologies when all negations (hence also <->c) are interpreted as true).  But if I interpreted the article cited below correctly, the lemma, hence the first statement (since it implies the lemma in minimal logic, if I made no mistake) are NOT minimalistic.

So to summarize, they hold in minimal logic plus ex-falso (intuitionistic logic) and in minimal logic plus Peirce (classical-refutability logic), but do not hold in minimal logic.

The paper is

  Hannes Diener and Maarten McKubre-Jordens,Classifying Material Implications over Minimal Logic, arXiv:1606.08092

where your lemma is proved to be equivalent over minimal logic to what they call the "weak Tarski formula"

  ( -. p -> -. -. ( p -> q ) )

which is proved to be not minimalistic by using a Kripke model.

Benoît