associativity of `↔`

Stream: lean4

[Kevin Buzzard]

variable (P : Prop)
#check P ↔ P ↔ P -- error
/-
P ↔ P : Prop
expected command
-/

Because I still don't understand how to check binding power of notation I can't figure out whether ↔ is supposed to be left or right associative, but the parser doesn't seem to fancy either choice here; it consumes P ↔ P and then decides it's all over.

[Julian Berman]

infix:20 " ↔ " => Iff

[Julian Berman]

(from https://github.com/leanprover/lean4/blob/292bab5a11dc05e019068a579a42eac251bf587f/src/Init/Core.lean#L45 )

[Mario Carneiro]

Incidentally, ↔ is associative, although that's a classical theorem, not intuitionistic

[Mario Carneiro]

It appears that lean 4 has a new command infix which means non-associative (in lean 3 this is a synonym for infixl meaning left-associative)

[Kevin Buzzard]

example : ∀ (a : Prop), a ↔ a ↔ a := sorry -- fine
example : ∀ (P : Prop), P ↔ P ↔ P := sorry -- unknown identifier `P`

I think it's specific to P!

[Mario Carneiro]

I can't replicate

[Kevin Buzzard]

I'm on today's nightly.

example : ∀ (x : Prop), x ↔ x ↔ x := sorry -- compiles
example : ∀ (A : Prop), A ↔ A ↔ A := sorry -- fails on third A
example : ∀ (A : Prop), a ↔ a ↔ a := sorry -- compiles?!

[Mario Carneiro]

although this yields a very surprising result for me

example : ∀ (P : Prop), P ↔ P ↔ P :=
_ -- (∀ (P : Prop), P ↔ P) ↔ P

[Kevin Buzzard]

buzzard@ebony:~/lean-projects/mathlib4_experiments$ lean --version
Lean (version 4.0.0-nightly-2021-04-29, commit 40b17bc364dd, Release)

[Mario Carneiro]

just updated to that, still unchanged

[Mario Carneiro]

oh wait it's different in a clean file

[Mario Carneiro]

oh I see I had a variable P

[Mario Carneiro]

this should work for you

variable (P : Prop)
example : ∀ (P : Prop), P ↔ P ↔ P :=
_ -- (∀ (P : Prop), P ↔ P) ↔ P

[Kevin Buzzard]

I can replicate (∀ (P : Prop), P ↔ P) ↔ P

[Mario Carneiro]

and it makes sense why you would get unknown identifier with that parse

[Mario Carneiro]

on the other hand

example : P ↔ P ↔ P :=

doesn't parse at all, the second ↔ seems to have ultra low precedence

[Mario Carneiro]

I don't think this is non-associativity after all

[Mac]

Kevin Buzzard said:

I'm on today's nightly.

example : ∀ (x : Prop), x ↔ x ↔ x := sorry -- compiles
example : ∀ (A : Prop), A ↔ A ↔ A := sorry -- fails on third A
example : ∀ (A : Prop), a ↔ a ↔ a := sorry -- compiles?!

This is because it is being parsed as Mario Carneiro showed and then the unbound lowercase latin letters are being auto bound as specified in https://leanprover.github.io/lean4/doc/autobound.html

[Mac]

To quote from the page: "When Lean processes the header of a declaration, any unbound identifier is automatically added as an implicit argument if it is a single lower case or greek letter."

[Mario Carneiro]

I can confirm that infix is to blame:

variable (P : Prop)
infix:50 " # " => Eq
example : ∀ (P : Prop), P # P # P :=
_ -- (∀ (P : Prop), P ↔ P) ↔ P

changing infix for infixl or infixr causes the expected parse

[Kevin Buzzard]

Thanks @Mac -- I had remembered the Greek letters but forgotten that it also worked with lower case

[Yakov Pechersky]

Probably has to do with the fixity of the universal quantifier

[Mac]

Mario Carneiro said:

I can confirm that infix is to blame:

variable (P : Prop)
infix:50 " # " => Eq
example : ∀ (P : Prop), P # P # P :=
_ -- (∀ (P : Prop), P ↔ P) ↔ P

changing infix for infixl or infixr causes the expected parse

Recall that infix:50 " # " => Eq really means notation:50 lhs:51 " # " rhs:51 => Eq lhs rhs (https://leanprover.github.io/lean4/doc/syntax.html). As both sides have greater (numerical) precedence, neither side can now have a # b at all. So what happens is it falls down the precedence scale until reaches the universal quantifier, but then the precedence level resets inside the binder.

[Mac]

Though all this confusion is somewhat expected considering that P ↔ Q ↔ R is not a particularly well-formed statement in intuitionistic logic in the first place (using the binary biconditional). Neither associative approach, i.e. P ↔ (Q ↔ R) or (P ↔ Q) ↔ R, is generally desired. What you might want is a variadic biconditional that expands P ↔ Q ↔ R to P ↔ Q /\ Q ↔ R, which could be done in a manner similar to the tuple notation.

[Mario Carneiro]

Actually I think a better way to parse non-associative operators is to allow them, say, as left associative, but then throw an explicit error during macro expansion

[Mac]

Mario Carneiro said:

Actually I think a better way to parse non-associative operators is to allow them, say, as left associative, but then throw an explicit error during macro expansion

That is certainly another option. Though I personally prefer that option that gives it meaning rather than one that deprives it of any. However, I do agree that, in the absence of a variadic version, an error is generally much more preferable than a cryptic parse.

[Kevin Buzzard]

The only reason all this started was that I was porting a Lean 3 file which used P \iff P \iff true

[Mac]

Kevin Buzzard said:

The only reason all this started was that I was porting a Lean 3 file which used P \iff P \iff true

Lol. This is why explicit parentheses are sometimes a very good thing. :)

[Kevin Buzzard]

But in lean 3 I just look up the associativity of the operator and then I know how to parse. I still haven't really understood why this isn't going on in lean 4 although I do understand what's happening now you flagged the lower case issue

[Mac]

Kevin Buzzard said:

But in lean 3 I just look up the associativity of the operator and then I know how to parse.

As far as I am aware, the same thing is true in Lean 4? Look up the definition of the notation and from there you can tell the precedence (the #) and the associativity, be it left (infixl), right (infixr) or none (infix).

[Kevin Buzzard]

My understanding of lean 3 was that you only had two options depending on whether the binding power of the second variable was equal to the first or one less

[Mac]

Ah, yeah, Lean 4 has expanded upon that.

[Mario Carneiro]

The point of non-associative operators is to force people to write the parentheses one way or another, exactly for cases like these where it's hard to guess

[Mario Carneiro]

which is why depriving that combination of operators of meaning is exactly the point. It's certainly better than the current behavior which is way outside what anyone would reasonably guess

[Mac]

True. I was just saying variadic operators would be nice alternative too.

[Eric Wieser]

Has a conscious choice been made by lean4 to not allow x rel y rel z (eg 0 ≤ i ≤ j < n) as a shorthand for x rel y \and y rel z like python, or is that still something that might be considered in future?

[Eric Wieser]

Or can such a feature be built easily with a macro?

[Sebastian Ullrich]

It is definitely not the right semantics for all operators - a \ne b \ne c is usually meant to also imply a \ne c, for example. So I think we will leave such extensions to the community.

[Sebastian Ullrich]

infixr:50 (priority := high) " = " => Eq
macro_rules
  | `($a = $b = $c) => `($a = $b ∧ $b = $c)

#check 1 = 2
#check 1 = 2 = 3
#check 1 = 2 = 3 = 4

[Kevin Buzzard]

Personally I get annoyed by people writing a \ne b \ne c to also imply a \ne c because I can't ever understand the logic which is supposed to let me deduce this, but I agree that I've seen this convention used in the wild.

[Mario Carneiro]

I would rather have a = b = c = d expand to tfae [a, b, c, d]. In any case, my point was only for the default handling of infix. For specific operators it is possible to provide an alternative macro interpretation, especially if the normal one is explicitly declaiming responsibility.

[Kevin Buzzard]

I think I like this idea that infix and infixl and infixr are three different things. Not everything has to parse, and I have had issues with students being confused when doing group theory from scratch because I state associativity as (a * b) * c = a * (b * c) and Lean prints it as a * b * c = a * (b * c). I think that in Lean 3 there was no way of making the prettyprinter print the thing which all the maths books would write when explaining associativity, and now one could do this temporarily and then actively switch it off later when you're sick of it, and the students will understand better.

[Mac]

Kevin Buzzard said:

I think I like this idea that infix and infixl and infixr are three different things. Not everything has to parse, and I have had issues with students being confused when doing group theory from scratch because I state associativity as (a * b) * c = a * (b * c) and Lean prints it as a * b * c = a * (b * c). I think that in Lean 3 there was no way of making the prettyprinter print the thing which all the maths books would write when explaining associativity, and now one could do this temporarily and then actively switch it off later when you're sick of it, and the students will understand better.

This actually precisely why I like the variadic operator approach for things like addition and multiplication. It makes (a * b * c) distinct from (a * b) * c and a * (b * c) so the pretty printer will keep them all separate.

[Mac]

Kevin Buzzard said:

Personally I get annoyed by people writing a \ne b \ne c to also imply a \ne c because I can't ever understand the logic which is supposed to let me deduce this, but I agree that I've seen this convention used in the wild.

Unfortunately, I am in camp a \ne b \ne c implies a \ne c. To me, the variadic \ne means mutual distinction, just as the variadic = means mutual equality.

[Scott Morrison]

Variadic ne is just weird. I don't think I've ever seen it in a paper!

[Mario Carneiro]

I am in the camp that says ne is infix and a \ne b \ne c is ambiguous and should be avoided

[Kevin Buzzard]

I might not have seen it in a paper but I've seen it on a blackboard (and winced)

[Damiano Testa]

I mentally add an extra \ne a, for my mental sanity, when I see it...

[Damiano Testa]

https://xkcd.com/859/

[Jakob von Raumer]

Damiano Testa said:

I mentally add an extra \ne a, for my mental sanity, when I see it...

That only works for three variables, though. With four variables you can at least still draw a graph with $\neq$-edges on the blackboard, with five variables, that graph isn't planar anymore ;)

[Sebastian Ullrich]

Now that's just planar silly

[Eric Wieser]

Just do a ≠ b ≠ c ≠ a ≠ d ≠ c ≠ d ≠ b...

[Eric Wieser]

Any path through the graph covering every edge is fine!

[Mario Carneiro]

You can't do that without repeating yourself somewhere for even n > 2

[Eric Wieser]

Yeah, I meant that as a joke

[Alena Gusakov]

I tend to write a \ne b, c, i feel like that's less ambiguous

[Alena Gusakov]

Unless b \ne c is also part of it

[Alena Gusakov]

I've seen profs write a \ne b \ne c before and I don't like it

[Mac]

Jakob von Raumer said:

Damiano Testa said:

I mentally add an extra \ne a, for my mental sanity, when I see it...

That only works for three variables, though. With four variables you can at least still draw a graph with $\neq$-edges on the blackboard, with five variables, that graph isn't planar anymore ;)

This actually why I like this definition of variadic ≠, it means that a ≠ b ≠ c ≠ d ≠ e is shorthand for a much longer set of ≠s. In fact, if I remember my math right, an ≠ of arity N is equal to N choose 2 manually written ≠s, which is some nice space savings. :)

[Eric Wieser]

Probably you want list.pairwise ne [a,b,c,d] at that point though, or similar

[Eric Wieser]

Else actually constructing or dissecting the terms would be awful

[Mac]

Eric Wieser said:

Probably you want list.pairwise ne [a,b,c,d] at that point though, or similar

Well, yeah, that would be the logical expansion, yes. Just like @Mario Carneiro mentioned that a = b = c = d could be expanded to tfae [a,b,c,d], a ≠ b ≠ c ≠ d could be expanded to list.pairwise ne [a,b,c,d]

[Mario Carneiro]

I think the notation itself is problematic though

[Mario Carneiro]

It could be expanded to that, yes. I don't think it's a good idea

[Mario Carneiro]

if you want pairwise ne then say so

[Mac]

When I read a ≠ b ≠ c ≠ d that is what I expect (pairwise ne) and that is also the way I would prefer pairwise ne to be denoted. I guess this just a place where we disagree on style.

[Mario Carneiro]

For one thing, if it is expanded that way, then it won't be obvious that you should be looking in the pairwise namespace for lemmas about a ≠ b ≠ c ≠ d

[Mario Carneiro]

unless there are just two things in which case you should look at ne

[Mario Carneiro]

that kind of clever expansion seems like it would confuse more than help

[Mac]

Mario Carneiro said:

For one thing, if it is expanded that way, then it won't be obvious that you should be looking in the pairwise namespace for lemmas about a ≠ b ≠ c ≠ d

I would probably define something like def mutual_distinction := list.pairwise ne and have it expand to mutual_distinction instead (and have theorems on mutual_distinction

[Mario Carneiro]

sure, same difference

[Mario Carneiro]

the notation doesn't say mutual_distinction so how will you know to look there?

[Mac]

That's what I would assume a ≠ b ≠ c ≠ d means

[Mario Carneiro]

I mean the words "mutual distinction" appear nowhere

[Mac]

In fact I would argue that is also what a ≠ b means

[Mario Carneiro]

this is a non-discoverable bit of magic syntax

[Mac]

In the same vein: how do I know that ≠ means ne, where is that written in the notation?

[Mario Carneiro]

If a ≠ b means mutual_distinction [a, b], then how do you say ne a b?

[Mac]

mutual_distinction [a, b] and ne [a, b] are defeq in my book..

[Mario Carneiro]

ne is a binary operator defined as a = b -> false

[Mario Carneiro]

which exists regardless of whether mutual_distinction exists

[Mario Carneiro]

Same thing with eq a b, we can't have everything be n-ary

[Mac]

If you are going by the current Lean Core, yes? This is about alternative definitions (as Lean doesn't currently have a variadic ne)

[Mario Carneiro]

No, I'm talking about what it could/should be

[Mario Carneiro]

It would be very disruptive if Eq was not a binary operator

[Mac]

Well then I don't agree that ne should actually always be defined as a = b -> false

[Mario Carneiro]

Okay, so when I want a = b -> false what do I write?

[Mac]

that?

[Mario Carneiro]

I submit that the vast majority of the time when ne is used it is binary and means that

[Mario Carneiro]

adding an indirection through mutual_distinction would make things worse for the majority of applications

[Mac]

I disagree, there are entire logics where a = b -> false is not a valid construction (and yet ne exists)

[Mario Carneiro]

?

[Mario Carneiro]

We're talking about lean, yes?

[Mac]

Yes, and you can construct alternative logics in Lean.

[Mario Carneiro]

If you want to make not not mean p -> false that is considerably more disruptive

[Mac]

Yes, true, but sometimes that is desired.

[Mario Carneiro]

Okay but in an alternative logic the notations are not my business

[Mario Carneiro]

I'm talking about general mathematics a la mathlib

[Mac]

Well, in my opinion, it is just like +, = and ≠ should just be defined based on classes that are defined differently for different types

[Mario Carneiro]

Eq is a typeclass now? Equality is a core concept of DTT, you can't get away from it and lean isn't really set up for that

[Mac]

I would define them something like the following:

universes u v

class Eq (P : Sort u) (T : Sort v) :=
  eq : T -> T -> P

class Ne (P : Sort u) (T : Sort v) :=
  ne : T -> T -> P

This definition, afaik, is entirely compatible with the current definition of the two in Lean.

[Yakov Pechersky]

Eq is heq, no?

[Mac]

No, HEq is heq

[Mario Carneiro]

One issue with that definition is that you can't write h : a = b because a = b isn't necessarily a type

[Mac]

The Prop instances (their current definitions) would look like the following:

@[defaultInstance low] instance {a : Sort v}: Eq Prop a := {eq := ...}
@[defaultInstance low] instance {a : Sort v}: Ne Prop a := {ne := ...}

[Mario Carneiro]

Is P an outparam? I think it needs to be if you don't want lots of inference issues

[Mac]

The defaulting will resolve that (afaik)

[Mac]

(same reason you don't get all kinds of issues with inference with Nat literals)

[Mario Carneiro]

What is the advantage of doing this? It won't make Eq the inductive type go away

[Mac]

I makes Lean's core (and the notation) more general, allowing it to be used more easily in alternative use cases (such as mine).

[Mario Carneiro]

What is your use case?

[Mac]

I am writing a metalogic in Lean 4.

[Mac]

Each logic thus has its own Prop type (and thus possibly its own definition of equality).

[Mario Carneiro]

Okay, that's been done in lean 3 and it doesn't require eliminating =

[Mario Carneiro]

You can overload the syntax if you really want to, but I wouldn't recommend it

[Mario Carneiro]

because you need that equality for metatheory reasoning

[Mac]

So what, you want to always write L |- eq a b instead of the cleaner L |- a = b?

[Mario Carneiro]

no, I would use some other = like symbol

[Mario Carneiro]

I think flypitch used \simeq

[Mac]

But, it is equality?

[Mario Carneiro]

No it's not equality

[Mario Carneiro]

it's provable equivalence in the theory

[Mario Carneiro]

equality is equality of terms which is something else

[Mac]

Which is what Lean's Eq is: provable equivalence in Lean's theory?

[Mario Carneiro]

Lean is the metatheory

[Mario Carneiro]

your logic is the theory

[Mac]

I am aware?

[Mario Carneiro]

You can only say that Eq is not true equality if you can step outside lean, which only works inside tactics and such

[Mario Carneiro]

if you are doing mathematics in lean then Eq is equality

[Mac]

Maybe you and I have different ideas of what qualifies as "true equality"

[Mario Carneiro]

It depends on the metalogic we are working in

[Mac]

Honestly, I am not even sure I agree that there is a "true equality" (except maybe identity -- and Lean's equality is most certainly not that)

[Mario Carneiro]

identity is just another word for equality

[Mac]

I disagree?

[Mario Carneiro]

Lean's equality is equality in the mathematical sense, provided we are not doing lean metatheory

[Mac]

No its not? Considering that defeq and Eq are not synonymous?

[Mario Carneiro]

if we are using lean as a metatheory for another logic then that logic has provable equivalence and lean has equality

[Mario Carneiro]

defeq is a metatheoretic notion

[Mac]

But as a result Lean's Eq does not satisfying the axioms of logical equality over Lean programs

[Mario Carneiro]

Huh?

[Mario Carneiro]

Eq certainly does satisfy the axioms of equality

[Mario Carneiro]

because we axiomatize it to be so

[Mac]

within proofs, yes, but not within Lean as a whole.

[Mario Carneiro]

I'm not sure what that means. In lean's logic, Eq is equality

[Mac]

A theory with logical equality should not be able (within the theory) to distinguish between two equal terms

[Mac]

Lean can, thus its Eq is not exactly true equality -- but I think you are said that when you were talking about tactics.

[Mario Carneiro]

How can it?

[Mac]

tactics can distinguish between defeq and Eq terms?

[Mac]

I feel like we are going very deep on a tangent that I am not sure is that important.

[Mario Carneiro]

tactics work in meta-lean, they can see distinctions that lean can't just as lean can see differences between provably equal terms in your logic

[Mac]

Mario Carneiro said:

tactics work in meta-lean, they can see distinctions that lean can't just as lean can see differences between provably equal terms in your logic

What do you consider to be Lean? I would certainly consider tactics part of Lean.

[Mario Carneiro]

I mean the lean logic

[Mac]

After all, you can prove things about them within Lean.

[Mac]

So there are two Lean logics then in your view? The Lean metalogic (used in tactics) and the Lean logic (where Eq is logical equality)?

[Mario Carneiro]

Eh, things get complicated if you do that. It's true that lean's tactics are expressed in lean's logic, but there are unverified bits performing the reflection, compilation and such

[Mario Carneiro]

It's certainly easiest to view them as entirely separate systems

[Mac]

Yes, but in Lean 4, all that is now writing in Lean, and can be dealt with in Lean proper.

[Mario Carneiro]

The fact that lean 4 is implemented in lean is incidental to this discussion

[Mac]

In fact isn't one of the main long-term goals of Lean 4 to verify Lean's parser/compiler in Lean?

[Mario Carneiro]

The lean kernel is not implemented in lean (yet)

[Mario Carneiro]

I don't know about that... I've suggested as much before but it seems that the developers have no intention of doing that themselves (although I think they would be fine with someone else doing it)

[Mario Carneiro]

Certainly partial is one roadblock to doing that in today's lean 4

[Mac]

Well yes, but that is partly due to the limitations of well-founded recursion in current Lean 4.

[Mac]

Also, so is the Lean logic (in your view) that which is verified by the kernel? Though, aren't tactics verified by the kernel too? After all, it verifies proofs.

[Mario Carneiro]

Yes, and yes (although calling tactics "verified by the kernel" is a bit of a stretch - they are typechecked)

[Mario Carneiro]

As an analogue, perhaps it helps to consider that peano arithmetic is a logic that is capable of talking about other logics, including peano arithmetic. It can serve as its own metalogic

[Mario Carneiro]

lean is doing something similar when you talk about lean tactics being objects in lean's logic

[Mario Carneiro]

But it is best to keep them separate, name them PA(meta) and PA(object) if you need to

[Mario Carneiro]

Perhaps "identity" and "equality" for you mean meta-= vs object-=

[Mario Carneiro]

When writing mathematics in lean, I treat lean as the object logic and mostly ignore the meta lean stuff except insofar as it affects proof construction techniques (i.e. what tactics to call)

[Mac]

"identity" for me means syntactic equality, but that is a fair alternative definition,

[Mac]

Mario Carneiro said:

When writing mathematics in lean, I treat lean as the object logic and mostly ignore the meta lean stuff except insofar as it affects proof construction techniques (i.e. what tactics to call)

That is a fair approach. It is simply not mine.

[Mario Carneiro]

When doing metamathematics in lean, it gets one step more complicated because we also get theory T and lean(object) is the metatheory for T

[Mac]

I treat Lean more as the basic system by which to express my notions. I actually try to avoid Lean Eq as it destroys syntactic equality which is what I want to try to keep as my background equality.

[Mario Carneiro]

For example, one place where Eq would come up when doing metamathematics is in defining substitution, which is an operation on terms

[Mario Carneiro]

you might have a theorem that says (P x)[a -> b] = P[a -> b] x[a -> b] where = is lean's =

[Mario Carneiro]

Equality comes up in a few places when defining proof rules. For example modus ponens, |- P => |- P -> Q => |- Q, is asserting equality between the two instances of P

[Mario Carneiro]

not equality in the theory, "syntactic equality", which since lean is the metatheory means Eq

[Mac]

Mario Carneiro said:

not equality in the theory, "syntactic equality", which since lean is the metatheory means Eq

With all the macros and parsers, this is no longer entirely true.

[Mario Carneiro]

the macros and parsers don't matter for this

[Mario Carneiro]

they are all meta-lean

[Mario Carneiro]

we're using lean to write the proof theory for some axiom system T here

[Mario Carneiro]

meta-lean is only there to help us automate the construction of the inductive types defining provability and so on

[Mac]

Also how does " For example modus ponens, |- P => |- P -> Q => |- Q, is asserting equality between the two instances of P" hold. Modus Ponens is not symmetric, equality is.

[Mac]

Modus Ponens is a rewrite/reduction rule, not an equivalence rule.

[Mario Carneiro]

I'm saying that MP(h, h2) is a proof of |- Q provided h proves |- P, h2 proves |- P' -> Q, and P = P' where = is @Eq term

[Mac]

Ah

[Mario Carneiro]

as a rough sketch, that might look like this in lean:

/-- Terms of theory T -/
inductive term
| imp : term → term → term
open term

/-- Provable terms in theory T -/
inductive proof : term → Prop
| mp {P Q} : proof P → proof (imp P Q) → proof Q

example {P P' Q} (h : proof P) (h2 : proof (imp P' Q)) (e : P = P') : proof Q :=
by cases e; exact proof.mp h h2

[Mac]

That looks pretty familiar to me! XD
Considering that I am writing a metalogic in Lean, I have a definition very similar to this already.

[Mario Carneiro]

The observation I want to make here is that the = in e is lean's interpretation of "syntactic equality"

[Mario Carneiro]

if you step up a metalevel you will say "that's not syntactic equality! This is syntactic equality!" but you can keep playing that game

[Mario Carneiro]

at every level there is some = relation that the logic thinks is equality and is valid up to the rules of the logic

[Mac]

Well then there is also just real syntactic equality? What you are describing is what I would call logical equality.

[Mario Carneiro]

Again, one person's syntactic equality is another's logical equality

[Mario Carneiro]

what meta-lean thinks is syntactic equality is just logical equality in meta-meta-lean

[Mac]

No? Syntactically equality is equality of strings "a" = "a", "a" ne "b"?

[Mario Carneiro]

That looks exactly like the way logical equality of strings is defined

[Mac]

Yes within a logic

[Mac]

Syntactic equality is formal language concept, not a logical concept

[Mac]

At least in my view.

[Mario Carneiro]

Syntactic equality is formal language concept

Yes, that formal concept being equality, within the logic of the formalism itself

[Mac]

A logic can define an equality that does or does not mirror syntactic equality on the language, but that is different

[Mac]

I am curious, what is your position the philosophy of mathematics, are you a formalist or logicist (or something else)?

[Mario Carneiro]

Formalist, of course :oops:

[Mac]

? Well that makes me confused.

[Mac]

Because, afaik, formalism generally asserts that the notion of strings (and their identity) comes first before logic.

[Mac]

Which is my position

[Mario Carneiro]

Whenever you look at a logical system from a meta-perspective, all the things that used to look like "actual equality" become "equality in the theory" or what you call "logical equality", and you gain access to another more precise "actual equality", which you might call "syntactic equality"

[Mario Carneiro]

But any formal system can be meta-ified

[Mac]

My point is that there exists (imo) a notion of equality that lies outside of logic.

[Mario Carneiro]

Sure, there is some philosophical notion of equality but I would not generally admit something like "a" = "a" under that because the two a's have different positions in space

[Mac]

This notion may or may not be the concept which a given logic chooses to formalize as "equality"

[Mac]

Mario Carneiro said:

Sure, there is some philosophical notion of equality but I would not generally admit something like "a" = "a" under that because the two a's have different positions in space

Which is why the abstraction of characters and strings is need, only then can the philosophical notion bet applied. Neither of these, however, requires formal logic. At least from my formalist perspective. In fact, in my view, formal logic can only defined after these notions are grasped.

[Mario Carneiro]

Logic is a way to analyze and formalize relations and concepts we believe extra-logically

[Mac]

Formal logics can then, of course, formalize these notions within themselves.

[Mario Carneiro]

and since formal logic can be applied to any mathematical field, including itself, you get this meta business

[Mac]

Mario Carneiro said:

Logic is a way to analyze and formalize relations and concepts we believe extra-logically

That strikes me more as a statement of Logicism https://en.wikipedia.org/wiki/Logicism than Formalism https://en.wikipedia.org/wiki/Formalism_(philosophy_of_mathematics)

[Mac]

To quote from the page "In the philosophy of mathematics, formalism is the view that holds that statements of mathematics and logic can be considered to be statements about the consequences of the manipulation of strings (alphanumeric sequences of symbols, usually as equations) using established manipulation rules." (Emphasis mine)

[Mario Carneiro]

I don't disagree with that

[Mario Carneiro]

Mathematics is a game of symbols on a page

[Mario Carneiro]

or in the computer, as it were

[Mac]

As someone who considers myself a formalist more than a logicism (by these definitions) I would thus disagree with your definition of Logic.

[Mac]

Though I would also somewhat agree.

[Mac]

For me, "Reason" is closer to what you defined to be "Logic" and "Logic" is the manipulation of strings.

[Mario Carneiro]

I'm not sure it is especially productive, but I would disagree with the logicist claim that everything is or is reducible to logic. But I would agree that mathematics can be analyzed using logic

[Mac]

However, a fair alternative definition is "Logic" as you defined and "Formal Logic" as I have defined.

[Mac]

Mario Carneiro said:

I'm not sure it is especially productive, but I would disagree with the logicist claim that everything is or is reducible to logic. But I would agree that mathematics can be analyzed using logic

Logicism just claims that everything in mathematics reduces to logic (not everything in general). Do you disagree with that?

[Mario Carneiro]

depends on what "reduces to" means

[Mario Carneiro]

limiting to mathematics seems prudent

[Mac]

Mario Carneiro said:

depends on what "reduces to" means

Hence why the Wikipedia article phrases it 3 different ways: "mathematics is an extension of logic, some or all of mathematics is reducible to logic, or some or all of mathematics may be modelled in logic" XD

[Mario Carneiro]

If you rephrase something enough times it's hard to disagree with

[Mac]

Lol!

[Mac]

I think the key thrust of my point is this: I consider that abstraction of characters and strings and their identity (which I term "syntactic equality" or "identity") to be a more fundamental concept than "logic".

[Mario Carneiro]

In any case, when modelling logic in lean, that notion is Eq

[Mac]

"logic"s can (and may or may not) model these concepts but they exist (and can be conceived of) without them

[Mario Carneiro]

When viewing lean itself as a logic it is not

[Mac]

Mario Carneiro said:

In any case, when modelling logic in lean, that notion is Eq

No. In fact Eq to a certain extent prevents the true notion of "syntactic equality" from being modelled (in my view).

[Mac]

As syntactically distinct things such as '1 + 1' and '2' can be considered Eq and can be substituted with one another in proofs (prohibiting distinction)

[Mario Carneiro]

1+1 is just a way to denote 2, says lean

[Mac]

Logical equality undermines syntactic equality.

[Mario Carneiro]

if you want 1+1 in the logic you would use term.add term.one term.one

[Mario Carneiro]

and lean will agree that this is not term.two

[Mac]

Mario Carneiro said:

1+1 is just a way to denote 2, says lean

Exactly! Thus Lean does not preserve syntactic equality (within itself).

[Mario Carneiro]

but the logic will agree that proof (prop.eq (term.add term.one term.one) term.two)

[Mac]

However, with the new metaprogramming capabilities this can be resolved by cheating in many cases.

[Mario Carneiro]

I feel like you are missing the point of mathematics, 1+1=2 is how it's supposed to work

[Mario Carneiro]

those two are the same number

[Mario Carneiro]

they aren't terms, they are two ways to write the same natural number

[Mac]

That's fine, in mathematics.

[Mario Carneiro]

yes, and lean is "mathematics" here

[Mario Carneiro]

and theory T is "the logic under study"

[Mac]

No, Lean can be much more general than that.

[Mac]

After all, it is now a general purpose programming language.

[Mario Carneiro]

But we're using it to do mathematics

[Mac]

My system is a metalogic and it needs to be able to represent logics where 1 + 1 is not exactly 2

[Mac]

They may be mathematically equal, but not equal in other ways.

[Mario Carneiro]

That requires that you use the language of the theory under study

[Mac]

Like in general programming.

[Mario Carneiro]

don't use Nat if you want that

[Mac]

Which I am not.

[Mario Carneiro]

If you have a term inductive then it is easy to make those two distinguishable

[Mac]

In computer science 1 + 1 is generally not logically equal to 2 (as one is a computation and one is a constant)

[Mario Carneiro]

I would argue that that is a meta-theoretic notion. The object language version of that is 1 + 1 == 2 and most programming languages will tell you that's true

[Mac]

Mario Carneiro said:

If you have a term inductive then it is easy to make those two distinguishable

Yeah, and I do do something like this.

[Mario Carneiro]

Certainly compilers seem to think that 1 + 1 is interchangeable with 2

[Mac]

Mario Carneiro said:

I would argue that that is a meta-theoretic notion. The object language version of that is 1 + 1 == 2 and most programming languages will tell you that's true

Yes, but when it comes to compiling/optimizing they are initially distinct.

[Mario Carneiro]

they are logically equal but syntactically different, in the language from earlier

[Mac]

The point of optimization is to pick the computational representation of two logically equivalent expressions that is more efficient (faster/less space), which requires you to be able to distinguish two logically equivalent terns.

[Mario Carneiro]

right, which works because compilers work at the meta-level with respect to the program logic

[Mac]

Correct, though, you can also do the same within a single logic by reducing the scope of equality.

[Mac]

i.e. by making mathematical equality not identical to logical equality.

[Mario Carneiro]

There are issues that crop up when you use a logic as its own metalogic. I think if the object-= and meta-= coincide it would have to be a fairly trivial logic

[Mac]

I disagree. In fact, I don't think equality is all that significant of a concept in the first place (to computation). For example, Peano arithmetic can be defined without it (or with just partial equality -- symmetric and transitive with no substitution).

[Mario Carneiro]

peano arithmetic at least lets you prove 1+1=2

[Mario Carneiro]

that theorem would fail if logical equality is exactly syntactic equality

[Mac]

For some definition of equality.

[Mario Carneiro]

for a very useful definition of equality

[Mac]

Peano equality is actually not logical equality (it does not have predicate substitution as one of its axioms).

[Mac]

It is only reflexive, transitive, and symmetric (and only for natural numbers).

[Mac]

https://en.wikipedia.org/wiki/Peano_axioms

[Mac]

It's closure property for nats is also not symmetric.

[Mac]

So if you have a = b where a is a nat and b is unknown you can't prove b is a nat.

[Mac]

With a = b, you con only prove the converse (i.e. if b is a nat, then a is a nat)

[Mac]

In fact, the lack of symmetry is why Peano arithmetic is so popular in computer science. Because its definitions really don't need symmetry.

[Mac]

They only need rewrite and joinability.

[Mario Carneiro]

PA builds on FOL, which generally has the substitution property either built in or derivable

[Mac]

Modern PA builds on FOL, original PA does not.

[Mac]

In fact, original PA is second-order.

[Mario Carneiro]

Mac said:

So if you have a = b where a is a nat and b is unknown you can't prove b is a nat.

This one is listed as number 5 on wiki

[Mac]

number 5 is the converse

[Mac]

Mac said:

With a = b, you con only prove the converse (i.e. if b is a nat, then a is a nat)

[Mario Carneiro]

equality is symmetric

[Mac]

Only for nats in PA.

[Mac]

number 3: "For all natural numbers x and y, if x = y, then y = x."

[Mac]

If b is unknown you can't use symmetry.

[Mac]

You first have prove that both sides are natural before you can use symmetry.

[Mario Carneiro]

That seems like a typo or oversight in the presentation

[Mac]

I wrote proofs of all these things to test my metalogic.

[Mac]

It works as formulated on the Wiki page.

[Mario Carneiro]

In formal treatments of this usually "is a natural number" isn't even a thing

[Mario Carneiro]

you just have all things be natural numbers

[Mac]

true, but some interesting prosperities emerge if you do it like written.

[Mac]

It also probably because PA is generally embedded in other logics rather than used on its own.

[Mario Carneiro]

Incidentally, I have been working for a while on a formal library which is based on PA; I don't know of any larger practical formal development using PA as the basis

[Mac]

Nat in Lean (and most other functional languages) is a embedding of (modern) PA?

[Mario Carneiro]

DTT is way stronger than PA

[Mac]

Yes, true

[Mario Carneiro]

I mean a formalization of the axiom system PA and its consequences

[Mario Carneiro]

yes, you can do this in lean (in principle)

[Mario Carneiro]

as far as I know no one has worked out a significant amount of mathematics in that setting

[Mac]

Well, now its done in practice.:)

[Mac]

I mostly just did it as a test of my system. I did find a lot of (what I consider to be) interesting results though.

[Mario Carneiro]

It's one thing to write the axioms and quite another to construct finite set theory in it, recursive functions, provability, and some CS stuff

[Mac]

Well yeah

[Mario Carneiro]

I would like lean 4 to get to the point that writing extended formal developments in embedded languages is easy; in lean 3 it's a pretty big ergonomic step down from regular lean proofs

[Mac]

What do you mean by an "embedded language"?

[Mario Carneiro]

like, in principle you can write tactics and things to work on the embedded language but for the most part you are starting from scratch

[Mario Carneiro]

I mean "theory T" that you are defining in lean

[Mario Carneiro]

like if you define the language and proof theory of PA and then want to prove a bazillion theorems in it because you want to prove godel incompleteness

[Mario Carneiro]

the reason for writing it in lean is so that you can also prove theorems about the system, but theorems in the system are also important

[Mac]

I think my approach is rather ergonomic to a degree. I don't know what others would think of it though. It is also in super super alpha.

[Mac]

You can more or less create one-for-one tactics.

[Mario Carneiro]

like it would be great if rw and simp could be made to work

[Mac]

I think the most annoying thing to work with though would be linear logic as you cannot reduce most things to functions any more.

[Mac]

Mario Carneiro said:

like it would be great if rw and simp could be made to work

Ah, then no, you would probably not like my approach then. I avoid those two commands like the plague.

[Mario Carneiro]

Hm, makes me wonder about porting Iris to lean 4

[Mario Carneiro]

why are you avoiding them?

[Mac]

I dislike rw and simp because they hide what rules/theorems you are actually using.

[Mario Carneiro]

if you are just trying to establish provability that's usually not a big deal

[Mac]

I want my proofs to be clear (and go to definition able)

[Mario Carneiro]

plus you can use simp only or only mark things as simp lemmas that you want to elide

[Mac]

Mario Carneiro said:

if you are just trying to establish provability that's usually not a big deal

True, but that is rarely my goal.

[Mac]

I am more interested in reverse mathematics.

[Mac]

i.e. I want to know exactly what assumptions were made to get to a given proof.

[Mac]

And I want to minimize them.

[Mario Carneiro]

That's what #print axioms is for

[Mario Carneiro]

well, you have more refined mechanisms for that in a deep embedding

[Mario Carneiro]

You can literally define a function on proofs that will tell you if you used only such and such assumptions

[Mac]

I like that stuff to be explicit. Also, print axioms only works for Lean axioms not other kinds of assumptions.

[Mac]

I also would like them to be readable in isolation from the source code.

[Mario Carneiro]

If you don't want to assume something, don't assume it

[Mac]

I want my lean proofs to more-or-less work (and be readable) in a vacuum.

[Mac]

And I am pretty happy with what I have gotten working in that regard.

[Mario Carneiro]

Those are not words I would use to describe lean

[Mario Carneiro]

there are quite a lot of things that go into turning lean text into a theorem/assertion

[Mac]

Here is my proof of commutativity of PA addition:

def addNatCommProof
{P : Sort u} {T : Sort v} {L : Logic P}
{N : PNat P T} {Q : SEq P T} {A : SAdd T}
(I   : NatInductionRight L N)
(NS  : NatSuccNat L N.toIsNat N.toSucc)
(NA  : NatAddNat L N.toIsNat A)
(QEL : EqNatLeftEuc L N.toIsNat Q)
(QtS : EqNatToEqSucc L N.toIsNat Q N.toSucc)
(A0C : AddNatZeroComm L N.toIsNat Q A N.toZero)
(ASn : AddSuccNatEqSucc L N.toIsNat Q A N.toSucc)
(AnS : AddNatSuccEqSucc L N.toIsNat Q A N.toSucc)
: (a b : T) -> (L |- nat a) -> (L |- nat b) -> (L |- a + b = b + a)
:= by
  refine natInductionRight ?f0 ?fS
  case f0 =>
    intro a Na
    exact addNatZeroComm Na
  case fS =>
    intro b Nb Anb_eq_Abn a Na
    have NSb := natS Nb
    have NAab := natAdd Na Nb; have NSAab := natS NAab;
    have NAba := natAdd Nb Na; have NSAba := natS NAba
    have NASba := natAdd NSb Na; have NASab := natAdd Na NSb
    apply eqNatLeftEuc NSAab NASab NASba
    exact addNatSuccEqSucc Na Nb
    apply eqNatLeftEuc NSAba NASba NSAab
    exact addSuccNatEqSucc Nb Na
    apply eqNatToEqSucc NAab NAba
    exact Anb_eq_Abn a Na

I still think it needs some refinement, but I like the general structure (and notation).

[Mac]

I do want to try to automate the nat proofs though.

[Mario Carneiro]

I'm not so sure about "readable in a vaccum" from this end

[Mario Carneiro]

have/apply/exact is not a great recipe for proofs that can be read offline

[Mac]

True

[Mac]

I do think my current orientation is more for reading in an editor sadly (with the goal info view).

[Mac]

My point here was mostly to demonstrate what I mean by making assumption/inference rules explicit

[Mac]

I think that part at least is readable in a vacuum.

[Mario Carneiro]

I would have preferred to see the actual statements rather than AddNatZeroComm

[Mac]

That's fair. My approach to that is one of things I want to fine. Though the actual statement approach can get a little verbose, and makes synthesizing derivative statements impossible (the reason they are written like this is to make them type classes).

[Mario Carneiro]

why aren't they in square brackets then?

[Mac]

Because they aren't being synthesized.

[Mario Carneiro]

I think that it would be better to just have a #print axioms like approach here, since listing the axioms on every theorem will get repetitive (for you and your readers)

[Mario Carneiro]

just add the ability to query the axioms used by any theorem

[Mac]

That's fair. I just personally don't like that approach myself (though I will admit adding the axioms to every theorem can be tiresome).

[Mario Carneiro]

For example, this metamath theorem is a proof of commutativity of and, and in the axiom list it says it depends on ax-1, ax-2, ax-3, ax-mp, and definitions df-bi, df-an

[Mac]

Though, also, I am not sure how I would do that.

[Mario Carneiro]

it's much easier for the computer to collect and organize this information, and it doesn't prevent the proof author from optimizing it

[Mario Carneiro]

In principle #print axioms does the same thing but because most of the DTT axioms aren't listed it has limited usefulness

[Mac]

I don't think Lean has a way of automatically inferring hypotheses though?

[Mario Carneiro]

No, they aren't hypotheses here, just axioms/theorems

[Mac]

They are hypotheses.

[Mario Carneiro]

In your version they are, but they can be set up as axioms

[Mario Carneiro]

and then you can track the usage of those axioms

[Mac]

How so?

[Mac]

They are attached to a specific logic.

[Mac]

They don't hold in a vacuum

[Mario Carneiro]

Yeah, the logic contains constructors for all the axioms

[Mario Carneiro]

like the proof inductive I showed earlier

[Mac]

no it does not

[Mac]

Not in my system

[Mario Carneiro]

which has a constructor for mp

[Mac]

In fact, many of the inference rules I have cannot be written DTT.

[Mario Carneiro]

??

[Mac]

as part of an inductive type

[Mario Carneiro]

I don't believe you :P

[Mac]

For example by conditional proof, ((L |- p) -> (L |- q)) -> (L |- p -> q)

[Mario Carneiro]

That's fine

[Mac]

If L was an inductive type this could not be written like that.

[Mario Carneiro]

well, actually it won't have the right effect

[Mario Carneiro]

that's not how imp introduction works

[Mario Carneiro]

The reason that doesn't work is that if p is independent then that proof rule says that p is false

[Mac]

Yes that is how conditional proof works (the mp was a typo).

[Mario Carneiro]

The right way to write it is (L, p |- q) => (L |- p -> q)

[Mario Carneiro]

basically you need the context to be an explicit part of the provability judgment

[Mario Carneiro]

at least, if you want gentzen style imp introduction rules

[Mac]

Mario Carneiro said:

The reason that doesn't work is that if p is independent then that proof rule says that p is false

What do you mean by this?

[Mac]

Mario Carneiro said:

The right way to write it is (L, p |- q) => (L |- p -> q)

I also don't know what that notation is meant to say.

[Mario Carneiro]

Suppose p is neither provable nor disprovable. Then L |- p is false, so L |- p -> L |- false is true, so L |- (p -> false) by your proof rule and so p is provably false. Thus every statement is provable or disprovable in the logic

[Mac]

"Suppose p is neither provable nor disprovable." That would mean that neither L |- p or (L |- p) -> False hold.

[Mario Carneiro]

No, It means that not (L |- p) and not (L |- not p)

[Mac]

L |- P is not (necessarily) a Prop

[Mario Carneiro]

doesn't really matter, use -> False if you like

[Mac]

L |- not p is not (necessarily) well-formed

[Mac]

That requires the language of L to have a not

[Mario Carneiro]

Okay... I am indeed making some bare minimum assumptions on the logic here

[Mario Carneiro]

if the logic doesn't have a false then perhaps it's not inconsistent if only because you can't express it

[Mac]

The logic is initially devoid of any rules and the prop is initially devoid of any syntax.

[Mario Carneiro]

Mac said:

Mario Carneiro said:

The right way to write it is (L, p |- q) => (L |- p -> q)

I also don't know what that notation is meant to say.

I'm not sure what L is, so let's add a context G, which is a list or set of formulas. The proof inductive is L, G |- p, and means that if we assume the formulas G then p follows. So in particular L, G |- p if p \in G. Then, the implication introduction rule is (L, p::G |- q) -> (L, G |- p -> q)

[Mac]

But yes with conditional proof, if I have (L |- p) -> False then L |- p -> q for all q. I don't see why that is a problem.

[Mario Carneiro]

Because you are lifting metalogical falsity into the logic

[Mario Carneiro]

That says "if p is not provable then p is disprovable"

[Mario Carneiro]

which is a very strong assumption

[Mario Carneiro]

in particular it is false for PA and ZFC and every other reasonable first order logic

[Mac]

If one wants a weaker assumption, feel free to use a weaker rule. But that, at least, is how I view the conditional proof rule to work.

[Mac]

If I can prove that (L |- p) does not hold, I can with the law of excluded middle, prove (L |- ~p) in most FO logic.

[Mario Carneiro]

The proof that L |- p does not hold is happening in the metalogic here

[Mario Carneiro]

for example, Godel's unprovable sentence

[Mario Carneiro]

It's not that the logic proves not p

[Mario Carneiro]

it is that the metalogic proves that L |- p is false, i.e. axiom system L does not prove p

[Mario Carneiro]

the law of excluded middle says L |- (p \/ ~p)

[Mac]

Incompleteness would be ((L |- p) \/ (L |- ~p) -> False), right? Not for a given p, (L |- p) -> False, correct?

[Mario Carneiro]

Yes. The first one says p is independent, and the second one says that p is not provable

[Mario Carneiro]

independent just means that neither p nor not p is provable

[Mario Carneiro]

but your axiom is essentially declaring that there are no independent sentences, which is also known as (syntactic) completeness

[Mac]

So it is saying that it implies that independence implies inconsistency, right?

[Mario Carneiro]

and Godel proved that such a system is inconsistent if it can handle basic arithmetic

[Mac]

Well, that is only true if the logical also includes FOL

[Mario Carneiro]

yes

[Mac]

If the metalogic is FOL (or DTT i.e. Lean), and the logic is just arithmatic that does not hold.

[Mario Carneiro]

there are complete axiom systems that are not strong enough for basic arithmetic

[Mario Carneiro]

but if it is strong enough to run godel's argument then it is inconsistent

[Mario Carneiro]

take a look at https://en.wikipedia.org/wiki/Proof_sketch_for_G%C3%B6del%27s_first_incompleteness_theorem to see whether your logic is weak enough; as long as it doesn't have FOL quantifiers or multiplication isn't total or something like that you might be able to get out of the issue

[Mac]

My point is that if you split the logic you can avoid that in many cases. For example, my fragment of PA is complete because only the equations and nat membership are statements in the logic. (It lacks quantifiers and propositional logical.)

[Mac]

Because all that is handled by the metalogic.

[Mario Carneiro]

If there are no quantifiers, then just have "all true sentences" as your axiom system and this is complete (and decidable)

[Mac]

Exactly

[Mario Carneiro]

in that case the L |- is just window dressing though

[Mac]

How so?

[Mario Carneiro]

you can prove L |- x = y <-> eval x = eval y more or less

[Mac]

Well I might not be able to evaluate x and y in the metalogic though by default.

[Mario Carneiro]

that's what I mean when I say it's decidable

[Mario Carneiro]

you can just lift the expressions into the metalogic

[Mario Carneiro]

you need some assumptions about plus and times

[Mario Carneiro]

but the ones in your sample proof should be close to all you need

[Mac]

Wait, but L is only a subset of the things provable in the metalogic.

[Mario Carneiro]

You will need to assume L is consistent for the reverse implication

[Mac]

like if I have (L |- 3 = 2) that does not mean that 3 = 2 in the metalogic.

[Mario Carneiro]

It does, if L is consistent

[Mac]

no it doesn't

[Mario Carneiro]

you might need something equivalent to not equal or less than in the logic

[Mac]

If I literally I have one axiom in I L, i.e L |- 3 = 2, that does not prove anything about 3 = 2 in the metalogic.

[Mario Carneiro]

normally you would be able to combine that with other axioms of L to prove L is inconsistent

[Mario Carneiro]

so if L is consistent then 3 = 2

[Mac]

consistency does not prove anything about the metalogic.

[Mac]

All consistency says is the ((p : P) -> (L |- p) /\ (L |- ~p) -> False)

[Mario Carneiro]

If L is consistent, and L |- 3 = 2, then (by using other axioms) L |- False and so L is inconsistent, contradiction, thus 3 = 2

[Mario Carneiro]

I'm assuming here that L is enough like PA that we can prove that L |- 3 != 2

[Mac]

If I have a logic with the propositions 3 = 2 ~(3 = 2) and the axiom L |- 3 = 2 that logic is both complete and consistent and says nothing about 3 = 2 in the metalogic

[Mario Carneiro]

You can use PA's other axioms to prove that 3 != 2

[Mac]

I am not talking about PA, I am just talking about some random logic L

[Mario Carneiro]

I'm talking about a random logic L with enough structure to run these arguments

[Mac]

That is sufficient structure.

[Mac]

A logic can be empty, it does not need proposition or rules.

[Mario Carneiro]

Okay but then you can't prove anything about it

[Mario Carneiro]

your earlier example had loads of assumptions about the logic

[Mario Carneiro]

I'm using those assumptions, more or less

[Mac]

Mac said:

If I have a logic with the propositions 3 = 2 ~(3 = 2) and the axiom L |- 3 = 2 that logic is both complete and consistent and says nothing about 3 = 2 in the metalogic

The logic here is a valid logic with 2 propositions and 1 axiom and is complete and consistent.

[Mario Carneiro]

yes

[Mario Carneiro]

I'm talking about a logic with at least x + 0 = x and x + s y = s (x+y)

[Mac]

Yeah but the PA fragment used to prove the semiring properities doesn't even need negation.

[Mac]

So it is trivially consistent

[Mario Carneiro]

If you add 3 = 2 to such a theory then you will get x = y for all x, y

[Mario Carneiro]

which is the nearest equivalent to inconsistency

[Mac]

Yes, if you add that to axiom list

[Mario Carneiro]

so if we assume that it is not inconsistent in that sense, then we will indeed have L |- x = y -> eval x = eval y

[Mario Carneiro]

and the converse is trivial by reflexivity

[Mac]

actually no, L |- S 0 = 1 in PA, but S 0 = 1 is not true in the metalogic (Lean).

[Mario Carneiro]

eval x = eval y

[Mac]

there is no eval (S 0) in the metalogic.

[Mario Carneiro]

the right side equality is equality in Nat

[Mario Carneiro]

there is, it's pretty easy to define

[Mac]

Yes, if I define S and 0 and 1 as there Nat counterparts true.

[Mac]

but if I define them all as separate terms, then no.

[Mario Carneiro]

the idea here is to turn any provability question L |- x = y into a statement eval x = eval y that we can just evaluate in lean

[Mac]

i.e.

inductive term
| zero : term
| one  : term
| succ : term -> term

[Mario Carneiro]

def eval : term -> Nat
| term.zero => 0
| term.one => 1
| term.succ x => eval x + 1

[Mac]

Well, yes because PA is embedded in Lean I can create an isomorphism between it and Lean, obviously.

[Eric Wieser]

Mario, your eval is not injective

[Notification Bot]

This topic was moved by Mario Carneiro to #Type theory > Metamathematics in lean 4