Zulip Chat Archive

Stream: lean4

Topic: associativity of `↔`


Kevin Buzzard (Apr 29 2021 at 22:42):

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 (Apr 29 2021 at 22:49):

infix:20 " ↔ " => Iff

Julian Berman (Apr 29 2021 at 22:49):

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

Mario Carneiro (Apr 29 2021 at 22:57):

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

Mario Carneiro (Apr 29 2021 at 23:00):

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 (Apr 29 2021 at 23:01):

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 (Apr 29 2021 at 23:03):

I can't replicate

Kevin Buzzard (Apr 29 2021 at 23:03):

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 (Apr 29 2021 at 23:04):

although this yields a very surprising result for me

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

Kevin Buzzard (Apr 29 2021 at 23:05):

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

Mario Carneiro (Apr 29 2021 at 23:06):

just updated to that, still unchanged

Mario Carneiro (Apr 29 2021 at 23:07):

oh wait it's different in a clean file

Mario Carneiro (Apr 29 2021 at 23:07):

oh I see I had a variable P

Mario Carneiro (Apr 29 2021 at 23:07):

this should work for you

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

Kevin Buzzard (Apr 29 2021 at 23:07):

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

Mario Carneiro (Apr 29 2021 at 23:08):

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

Mario Carneiro (Apr 29 2021 at 23:09):

on the other hand

example : P  P  P :=

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

Mario Carneiro (Apr 29 2021 at 23:10):

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

Mac (Apr 29 2021 at 23:16):

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 (Apr 29 2021 at 23:17):

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 (Apr 29 2021 at 23:17):

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 (Apr 29 2021 at 23:18):

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

Yakov Pechersky (Apr 29 2021 at 23:18):

Probably has to do with the fixity of the universal quantifier

Mac (Apr 29 2021 at 23:22):

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 (Apr 29 2021 at 23:27):

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 (Apr 29 2021 at 23:31):

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 (Apr 29 2021 at 23:35):

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 (Apr 29 2021 at 23:35):

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

Mac (Apr 29 2021 at 23:38):

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 (Apr 29 2021 at 23:39):

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 (Apr 29 2021 at 23:48):

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 (Apr 29 2021 at 23:49):

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 (Apr 29 2021 at 23:59):

Ah, yeah, Lean 4 has expanded upon that.

Mario Carneiro (Apr 30 2021 at 00:09):

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 (Apr 30 2021 at 00:10):

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 (Apr 30 2021 at 00:34):

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

Eric Wieser (Apr 30 2021 at 07:49):

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 (Apr 30 2021 at 07:51):

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

Sebastian Ullrich (Apr 30 2021 at 07:58):

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 (Apr 30 2021 at 07:58):

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 (Apr 30 2021 at 08:00):

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 (Apr 30 2021 at 11:13):

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 (Apr 30 2021 at 11:42):

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 (May 01 2021 at 01:42):

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 (May 01 2021 at 01:44):

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 (May 01 2021 at 02:19):

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

Mario Carneiro (May 01 2021 at 02:42):

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

Kevin Buzzard (May 01 2021 at 08:24):

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

Damiano Testa (May 01 2021 at 08:42):

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

Damiano Testa (May 01 2021 at 09:01):

https://xkcd.com/859/

Jakob von Raumer (May 02 2021 at 10:21):

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 (May 02 2021 at 10:24):

Now that's just planar silly

Eric Wieser (May 02 2021 at 10:47):

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

Eric Wieser (May 02 2021 at 10:48):

Any path through the graph covering every edge is fine!

Mario Carneiro (May 02 2021 at 11:37):

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

Eric Wieser (May 02 2021 at 11:54):

Yeah, I meant that as a joke

Alena Gusakov (May 02 2021 at 13:00):

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

Alena Gusakov (May 02 2021 at 13:01):

Unless b \ne c is also part of it

Alena Gusakov (May 02 2021 at 13:01):

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

Mac (May 02 2021 at 16:37):

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 (May 02 2021 at 16:38):

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

Eric Wieser (May 02 2021 at 16:39):

Else actually constructing or dissecting the terms would be awful

Mac (May 02 2021 at 16:42):

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 (May 02 2021 at 16:43):

I think the notation itself is problematic though

Mario Carneiro (May 02 2021 at 16:43):

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

Mario Carneiro (May 02 2021 at 16:43):

if you want pairwise ne then say so

Mac (May 02 2021 at 16:44):

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 (May 02 2021 at 16:45):

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 (May 02 2021 at 16:45):

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

Mario Carneiro (May 02 2021 at 16:46):

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

Mac (May 02 2021 at 16:46):

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 (May 02 2021 at 16:46):

sure, same difference

Mario Carneiro (May 02 2021 at 16:47):

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

Mac (May 02 2021 at 16:47):

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

Mario Carneiro (May 02 2021 at 16:47):

I mean the words "mutual distinction" appear nowhere

Mac (May 02 2021 at 16:47):

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

Mario Carneiro (May 02 2021 at 16:48):

this is a non-discoverable bit of magic syntax

Mac (May 02 2021 at 16:48):

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

Mario Carneiro (May 02 2021 at 16:49):

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

Mac (May 02 2021 at 16:49):

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

Mario Carneiro (May 02 2021 at 16:49):

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

Mario Carneiro (May 02 2021 at 16:50):

which exists regardless of whether mutual_distinction exists

Mario Carneiro (May 02 2021 at 16:50):

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

Mac (May 02 2021 at 16:51):

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 (May 02 2021 at 16:51):

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

Mario Carneiro (May 02 2021 at 16:51):

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

Mac (May 02 2021 at 16:52):

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

Mario Carneiro (May 02 2021 at 16:52):

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

Mac (May 02 2021 at 16:53):

that?

Mario Carneiro (May 02 2021 at 16:53):

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

Mario Carneiro (May 02 2021 at 16:53):

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

Mac (May 02 2021 at 16:53):

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

Mario Carneiro (May 02 2021 at 16:54):

?

Mario Carneiro (May 02 2021 at 16:54):

We're talking about lean, yes?

Mac (May 02 2021 at 16:55):

Yes, and you can construct alternative logics in Lean.

Mario Carneiro (May 02 2021 at 16:55):

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

Mac (May 02 2021 at 16:55):

Yes, true, but sometimes that is desired.

Mario Carneiro (May 02 2021 at 16:55):

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

Mario Carneiro (May 02 2021 at 16:56):

I'm talking about general mathematics a la mathlib

Mac (May 02 2021 at 16:56):

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 (May 02 2021 at 16:58):

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 (May 02 2021 at 16:58):

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 (May 02 2021 at 16:59):

Eq is heq, no?

Mac (May 02 2021 at 16:59):

No, HEq is heq

Mario Carneiro (May 02 2021 at 17:01):

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

Mac (May 02 2021 at 17:02):

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 (May 02 2021 at 17:02):

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

Mac (May 02 2021 at 17:03):

The defaulting will resolve that (afaik)

Mac (May 02 2021 at 17:04):

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

Mario Carneiro (May 02 2021 at 17:04):

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

Mac (May 02 2021 at 17:05):

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 (May 02 2021 at 17:05):

What is your use case?

Mac (May 02 2021 at 17:05):

I am writing a metalogic in Lean 4.

Mac (May 02 2021 at 17:06):

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

Mario Carneiro (May 02 2021 at 17:06):

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

Mario Carneiro (May 02 2021 at 17:07):

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

Mario Carneiro (May 02 2021 at 17:07):

because you need that equality for metatheory reasoning

Mac (May 02 2021 at 17:07):

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

Mario Carneiro (May 02 2021 at 17:07):

no, I would use some other = like symbol

Mario Carneiro (May 02 2021 at 17:08):

I think flypitch used \simeq

Mac (May 02 2021 at 17:08):

But, it is equality?

Mario Carneiro (May 02 2021 at 17:08):

No it's not equality

Mario Carneiro (May 02 2021 at 17:08):

it's provable equivalence in the theory

Mario Carneiro (May 02 2021 at 17:08):

equality is equality of terms which is something else

Mac (May 02 2021 at 17:08):

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

Mario Carneiro (May 02 2021 at 17:09):

Lean is the metatheory

Mario Carneiro (May 02 2021 at 17:09):

your logic is the theory

Mac (May 02 2021 at 17:09):

I am aware?

Mario Carneiro (May 02 2021 at 17:09):

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 (May 02 2021 at 17:10):

if you are doing mathematics in lean then Eq is equality

Mac (May 02 2021 at 17:10):

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

Mario Carneiro (May 02 2021 at 17:10):

It depends on the metalogic we are working in

Mac (May 02 2021 at 17:10):

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 (May 02 2021 at 17:11):

identity is just another word for equality

Mac (May 02 2021 at 17:11):

I disagree?

Mario Carneiro (May 02 2021 at 17:11):

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

Mac (May 02 2021 at 17:12):

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

Mario Carneiro (May 02 2021 at 17:12):

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

Mario Carneiro (May 02 2021 at 17:12):

defeq is a metatheoretic notion

Mac (May 02 2021 at 17:13):

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

Mario Carneiro (May 02 2021 at 17:13):

Huh?

Mario Carneiro (May 02 2021 at 17:13):

Eq certainly does satisfy the axioms of equality

Mario Carneiro (May 02 2021 at 17:13):

because we axiomatize it to be so

Mac (May 02 2021 at 17:14):

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

Mario Carneiro (May 02 2021 at 17:15):

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

Mac (May 02 2021 at 17:15):

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

Mac (May 02 2021 at 17:15):

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 (May 02 2021 at 17:16):

How can it?

Mac (May 02 2021 at 17:16):

tactics can distinguish between defeq and Eq terms?

Mac (May 02 2021 at 17:17):

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

Mario Carneiro (May 02 2021 at 17:17):

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 (May 02 2021 at 17:18):

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 (May 02 2021 at 17:18):

I mean the lean logic

Mac (May 02 2021 at 17:18):

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

Mac (May 02 2021 at 17:19):

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 (May 02 2021 at 17:19):

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 (May 02 2021 at 17:20):

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

Mac (May 02 2021 at 17:20):

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

Mario Carneiro (May 02 2021 at 17:20):

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

Mac (May 02 2021 at 17:21):

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

Mario Carneiro (May 02 2021 at 17:21):

The lean kernel is not implemented in lean (yet)

Mario Carneiro (May 02 2021 at 17:22):

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 (May 02 2021 at 17:22):

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

Mac (May 02 2021 at 17:23):

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

Mac (May 02 2021 at 17:23):

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 (May 02 2021 at 17:24):

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

Mario Carneiro (May 02 2021 at 17:26):

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 (May 02 2021 at 17:26):

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

Mario Carneiro (May 02 2021 at 17:27):

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

Mario Carneiro (May 02 2021 at 17:28):

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

Mario Carneiro (May 02 2021 at 17:29):

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 (May 02 2021 at 17:30):

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

Mac (May 02 2021 at 17:30):

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 (May 02 2021 at 17:31):

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 (May 02 2021 at 17:32):

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 (May 02 2021 at 17:32):

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

Mario Carneiro (May 02 2021 at 17:33):

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

Mario Carneiro (May 02 2021 at 17:35):

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 (May 02 2021 at 17:35):

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

Mac (May 02 2021 at 17:36):

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 (May 02 2021 at 17:36):

the macros and parsers don't matter for this

Mario Carneiro (May 02 2021 at 17:36):

they are all meta-lean

Mario Carneiro (May 02 2021 at 17:37):

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

Mario Carneiro (May 02 2021 at 17:38):

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

Mac (May 02 2021 at 17:38):

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 (May 02 2021 at 17:38):

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

Mario Carneiro (May 02 2021 at 17:39):

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 (May 02 2021 at 17:40):

Ah

Mario Carneiro (May 02 2021 at 17:43):

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 (May 02 2021 at 17:45):

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 (May 02 2021 at 17:45):

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

Mario Carneiro (May 02 2021 at 17:46):

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 (May 02 2021 at 17:47):

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

Mac (May 02 2021 at 17:47):

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

Mario Carneiro (May 02 2021 at 17:48):

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

Mario Carneiro (May 02 2021 at 17:49):

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

Mac (May 02 2021 at 17:49):

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

Mario Carneiro (May 02 2021 at 17:50):

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

Mac (May 02 2021 at 17:50):

Yes within a logic

Mac (May 02 2021 at 17:51):

Syntactic equality is formal language concept, not a logical concept

Mac (May 02 2021 at 17:51):

At least in my view.

Mario Carneiro (May 02 2021 at 17:52):

Syntactic equality is formal language concept

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

Mac (May 02 2021 at 17:52):

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

Mac (May 02 2021 at 17:53):

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

Mario Carneiro (May 02 2021 at 17:53):

Formalist, of course :oops:

Mac (May 02 2021 at 17:54):

? Well that makes me confused.

Mac (May 02 2021 at 17:54):

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

Mac (May 02 2021 at 17:54):

Which is my position

Mario Carneiro (May 02 2021 at 17:55):

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 (May 02 2021 at 17:55):

But any formal system can be meta-ified

Mac (May 02 2021 at 17:56):

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

Mario Carneiro (May 02 2021 at 17:57):

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 (May 02 2021 at 17:57):

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

Mac (May 02 2021 at 17:58):

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 (May 02 2021 at 17:59):

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

Mac (May 02 2021 at 17:59):

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

Mario Carneiro (May 02 2021 at 18:00):

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

Mac (May 02 2021 at 18:00):

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 (May 02 2021 at 18:01):

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 (May 02 2021 at 18:01):

I don't disagree with that

Mario Carneiro (May 02 2021 at 18:02):

Mathematics is a game of symbols on a page

Mario Carneiro (May 02 2021 at 18:02):

or in the computer, as it were

Mac (May 02 2021 at 18:02):

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

Mac (May 02 2021 at 18:02):

Though I would also somewhat agree.

Mac (May 02 2021 at 18:03):

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

Mario Carneiro (May 02 2021 at 18:03):

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 (May 02 2021 at 18:04):

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

Mac (May 02 2021 at 18:05):

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 (May 02 2021 at 18:05):

depends on what "reduces to" means

Mario Carneiro (May 02 2021 at 18:06):

limiting to mathematics seems prudent

Mac (May 02 2021 at 18:07):

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 (May 02 2021 at 18:08):

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

Mac (May 02 2021 at 18:09):

Lol!

Mac (May 02 2021 at 18:11):

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 (May 02 2021 at 18:12):

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

Mac (May 02 2021 at 18:12):

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

Mario Carneiro (May 02 2021 at 18:12):

When viewing lean itself as a logic it is not

Mac (May 02 2021 at 18:14):

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 (May 02 2021 at 18:15):

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 (May 02 2021 at 18:15):

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

Mac (May 02 2021 at 18:15):

Logical equality undermines syntactic equality.

Mario Carneiro (May 02 2021 at 18:15):

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

Mario Carneiro (May 02 2021 at 18:16):

and lean will agree that this is not term.two

Mac (May 02 2021 at 18:16):

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 (May 02 2021 at 18:16):

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

Mac (May 02 2021 at 18:16):

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

Mario Carneiro (May 02 2021 at 18:17):

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

Mario Carneiro (May 02 2021 at 18:18):

those two are the same number

Mario Carneiro (May 02 2021 at 18:18):

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

Mac (May 02 2021 at 18:18):

That's fine, in mathematics.

Mario Carneiro (May 02 2021 at 18:18):

yes, and lean is "mathematics" here

Mario Carneiro (May 02 2021 at 18:19):

and theory T is "the logic under study"

Mac (May 02 2021 at 18:19):

No, Lean can be much more general than that.

Mac (May 02 2021 at 18:19):

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

Mario Carneiro (May 02 2021 at 18:19):

But we're using it to do mathematics

Mac (May 02 2021 at 18:19):

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

Mac (May 02 2021 at 18:20):

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

Mario Carneiro (May 02 2021 at 18:20):

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

Mac (May 02 2021 at 18:20):

Like in general programming.

Mario Carneiro (May 02 2021 at 18:20):

don't use Nat if you want that

Mac (May 02 2021 at 18:20):

Which I am not.

Mario Carneiro (May 02 2021 at 18:21):

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

Mac (May 02 2021 at 18:21):

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

Mario Carneiro (May 02 2021 at 18:22):

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 (May 02 2021 at 18:22):

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 (May 02 2021 at 18:23):

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

Mac (May 02 2021 at 18:23):

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 (May 02 2021 at 18:24):

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

Mac (May 02 2021 at 18:25):

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 (May 02 2021 at 18:25):

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

Mac (May 02 2021 at 18:26):

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

Mac (May 02 2021 at 18:27):

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

Mario Carneiro (May 02 2021 at 18:28):

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 (May 02 2021 at 18:30):

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 (May 02 2021 at 18:30):

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

Mario Carneiro (May 02 2021 at 18:31):

that theorem would fail if logical equality is exactly syntactic equality

Mac (May 02 2021 at 18:31):

For some definition of equality.

Mario Carneiro (May 02 2021 at 18:31):

for a very useful definition of equality

Mac (May 02 2021 at 18:31):

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

Mac (May 02 2021 at 18:32):

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

Mac (May 02 2021 at 18:32):

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

Mac (May 02 2021 at 18:32):

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

Mac (May 02 2021 at 18:33):

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

Mac (May 02 2021 at 18:34):

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

Mac (May 02 2021 at 18:35):

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 (May 02 2021 at 18:36):

They only need rewrite and joinability.

Mario Carneiro (May 02 2021 at 18:36):

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

Mac (May 02 2021 at 18:36):

Modern PA builds on FOL, original PA does not.

Mac (May 02 2021 at 18:37):

In fact, original PA is second-order.

Mario Carneiro (May 02 2021 at 18:37):

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 (May 02 2021 at 18:37):

number 5 is the converse

Mac (May 02 2021 at 18:37):

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 (May 02 2021 at 18:38):

equality is symmetric

Mac (May 02 2021 at 18:38):

Only for nats in PA.

Mac (May 02 2021 at 18:38):

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

Mac (May 02 2021 at 18:38):

If b is unknown you can't use symmetry.

Mac (May 02 2021 at 18:39):

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

Mario Carneiro (May 02 2021 at 18:39):

That seems like a typo or oversight in the presentation

Mac (May 02 2021 at 18:40):

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

Mac (May 02 2021 at 18:40):

It works as formulated on the Wiki page.

Mario Carneiro (May 02 2021 at 18:40):

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

Mario Carneiro (May 02 2021 at 18:40):

you just have all things be natural numbers

Mac (May 02 2021 at 18:41):

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

Mac (May 02 2021 at 18:42):

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

Mario Carneiro (May 02 2021 at 18:43):

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 (May 02 2021 at 18:43):

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

Mario Carneiro (May 02 2021 at 18:44):

DTT is way stronger than PA

Mac (May 02 2021 at 18:44):

Yes, true

Mario Carneiro (May 02 2021 at 18:44):

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

Mario Carneiro (May 02 2021 at 18:45):

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

Mario Carneiro (May 02 2021 at 18:45):

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

Mac (May 02 2021 at 18:45):

Well, now its done in practice.:)

Mac (May 02 2021 at 18:46):

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 (May 02 2021 at 18:47):

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 (May 02 2021 at 18:48):

Well yeah

Mario Carneiro (May 02 2021 at 18:48):

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 (May 02 2021 at 18:49):

What do you mean by an "embedded language"?

Mario Carneiro (May 02 2021 at 18:49):

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 (May 02 2021 at 18:50):

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

Mario Carneiro (May 02 2021 at 18:50):

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 (May 02 2021 at 18:51):

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 (May 02 2021 at 18:51):

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 (May 02 2021 at 18:52):

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

Mario Carneiro (May 02 2021 at 18:52):

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

Mac (May 02 2021 at 18:52):

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 (May 02 2021 at 18:53):

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 (May 02 2021 at 18:53):

Hm, makes me wonder about porting Iris to lean 4

Mario Carneiro (May 02 2021 at 18:54):

why are you avoiding them?

Mac (May 02 2021 at 18:54):

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

Mario Carneiro (May 02 2021 at 18:55):

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

Mac (May 02 2021 at 18:55):

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

Mario Carneiro (May 02 2021 at 18:55):

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

Mac (May 02 2021 at 18:55):

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 (May 02 2021 at 18:55):

I am more interested in reverse mathematics.

Mac (May 02 2021 at 18:56):

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

Mac (May 02 2021 at 18:56):

And I want to minimize them.

Mario Carneiro (May 02 2021 at 18:56):

That's what #print axioms is for

Mario Carneiro (May 02 2021 at 18:56):

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

Mario Carneiro (May 02 2021 at 18:57):

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

Mac (May 02 2021 at 18:57):

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

Mac (May 02 2021 at 18:58):

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

Mario Carneiro (May 02 2021 at 18:58):

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

Mac (May 02 2021 at 18:59):

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

Mac (May 02 2021 at 19:00):

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

Mario Carneiro (May 02 2021 at 19:00):

Those are not words I would use to describe lean

Mario Carneiro (May 02 2021 at 19:02):

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

Mac (May 02 2021 at 19:02):

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 (May 02 2021 at 19:03):

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

Mario Carneiro (May 02 2021 at 19:05):

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

Mario Carneiro (May 02 2021 at 19:05):

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

Mac (May 02 2021 at 19:06):

True

Mac (May 02 2021 at 19:06):

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

Mac (May 02 2021 at 19:07):

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

Mac (May 02 2021 at 19:08):

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

Mario Carneiro (May 02 2021 at 19:08):

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

Mac (May 02 2021 at 19:12):

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 (May 02 2021 at 19:12):

why aren't they in square brackets then?

Mac (May 02 2021 at 19:13):

Because they aren't being synthesized.

Mario Carneiro (May 02 2021 at 19:14):

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 (May 02 2021 at 19:14):

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

Mac (May 02 2021 at 19:15):

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 (May 02 2021 at 19:16):

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 (May 02 2021 at 19:16):

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

Mario Carneiro (May 02 2021 at 19:16):

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 (May 02 2021 at 19:17):

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

Mac (May 02 2021 at 19:18):

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

Mario Carneiro (May 02 2021 at 19:19):

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

Mac (May 02 2021 at 19:19):

They are hypotheses.

Mario Carneiro (May 02 2021 at 19:19):

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

Mario Carneiro (May 02 2021 at 19:19):

and then you can track the usage of those axioms

Mac (May 02 2021 at 19:19):

How so?

Mac (May 02 2021 at 19:20):

They are attached to a specific logic.

Mac (May 02 2021 at 19:20):

They don't hold in a vacuum

Mario Carneiro (May 02 2021 at 19:20):

Yeah, the logic contains constructors for all the axioms

Mario Carneiro (May 02 2021 at 19:20):

like the proof inductive I showed earlier

Mac (May 02 2021 at 19:20):

no it does not

Mac (May 02 2021 at 19:20):

Not in my system

Mario Carneiro (May 02 2021 at 19:20):

which has a constructor for mp

Mac (May 02 2021 at 19:21):

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

Mario Carneiro (May 02 2021 at 19:21):

??

Mac (May 02 2021 at 19:21):

as part of an inductive type

Mario Carneiro (May 02 2021 at 19:21):

I don't believe you :P

Mac (May 02 2021 at 19:21):

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

Mario Carneiro (May 02 2021 at 19:22):

That's fine

Mac (May 02 2021 at 19:22):

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

Mario Carneiro (May 02 2021 at 19:22):

well, actually it won't have the right effect

Mario Carneiro (May 02 2021 at 19:22):

that's not how imp introduction works

Mario Carneiro (May 02 2021 at 19:23):

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

Mac (May 02 2021 at 19:23):

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

Mario Carneiro (May 02 2021 at 19:24):

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

Mario Carneiro (May 02 2021 at 19:24):

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

Mario Carneiro (May 02 2021 at 19:24):

at least, if you want gentzen style imp introduction rules

Mac (May 02 2021 at 19:24):

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 (May 02 2021 at 19:25):

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 (May 02 2021 at 19:26):

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 (May 02 2021 at 19:27):

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

Mario Carneiro (May 02 2021 at 19:28):

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

Mac (May 02 2021 at 19:29):

L |- P is not (necessarily) a Prop

Mario Carneiro (May 02 2021 at 19:29):

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

Mac (May 02 2021 at 19:29):

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

Mac (May 02 2021 at 19:29):

That requires the language of L to have a not

Mario Carneiro (May 02 2021 at 19:30):

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

Mario Carneiro (May 02 2021 at 19:30):

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

Mac (May 02 2021 at 19:30):

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

Mario Carneiro (May 02 2021 at 19:32):

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 (May 02 2021 at 19:33):

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 (May 02 2021 at 19:34):

Because you are lifting metalogical falsity into the logic

Mario Carneiro (May 02 2021 at 19:34):

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

Mario Carneiro (May 02 2021 at 19:34):

which is a very strong assumption

Mario Carneiro (May 02 2021 at 19:35):

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

Mac (May 02 2021 at 19:35):

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 (May 02 2021 at 19:41):

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 (May 02 2021 at 19:41):

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

Mario Carneiro (May 02 2021 at 19:42):

for example, Godel's unprovable sentence

Mario Carneiro (May 02 2021 at 19:42):

It's not that the logic proves not p

Mario Carneiro (May 02 2021 at 19:42):

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

Mario Carneiro (May 02 2021 at 19:43):

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

Mac (May 02 2021 at 19:43):

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

Mario Carneiro (May 02 2021 at 19:44):

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

Mario Carneiro (May 02 2021 at 19:44):

independent just means that neither p nor not p is provable

Mario Carneiro (May 02 2021 at 19:45):

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

Mac (May 02 2021 at 19:47):

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

Mario Carneiro (May 02 2021 at 19:47):

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

Mac (May 02 2021 at 19:47):

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

Mario Carneiro (May 02 2021 at 19:47):

yes

Mac (May 02 2021 at 19:47):

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

Mario Carneiro (May 02 2021 at 19:48):

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

Mario Carneiro (May 02 2021 at 19:48):

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

Mario Carneiro (May 02 2021 at 19:51):

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 (May 02 2021 at 19:51):

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 (May 02 2021 at 19:51):

Because all that is handled by the metalogic.

Mario Carneiro (May 02 2021 at 19:52):

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

Mac (May 02 2021 at 19:52):

Exactly

Mario Carneiro (May 02 2021 at 19:53):

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

Mac (May 02 2021 at 19:54):

How so?

Mario Carneiro (May 02 2021 at 19:54):

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

Mac (May 02 2021 at 19:55):

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

Mario Carneiro (May 02 2021 at 19:55):

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

Mario Carneiro (May 02 2021 at 19:55):

you can just lift the expressions into the metalogic

Mario Carneiro (May 02 2021 at 19:56):

you need some assumptions about plus and times

Mario Carneiro (May 02 2021 at 19:56):

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

Mac (May 02 2021 at 19:57):

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

Mario Carneiro (May 02 2021 at 19:57):

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

Mac (May 02 2021 at 19:58):

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

Mario Carneiro (May 02 2021 at 19:58):

It does, if L is consistent

Mac (May 02 2021 at 19:58):

no it doesn't

Mario Carneiro (May 02 2021 at 19:58):

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

Mac (May 02 2021 at 19:58):

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 (May 02 2021 at 19:59):

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

Mario Carneiro (May 02 2021 at 19:59):

so if L is consistent then 3 = 2

Mac (May 02 2021 at 19:59):

consistency does not prove anything about the metalogic.

Mac (May 02 2021 at 20:00):

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

Mario Carneiro (May 02 2021 at 20:01):

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 (May 02 2021 at 20:01):

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

Mac (May 02 2021 at 20:02):

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 (May 02 2021 at 20:03):

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

Mac (May 02 2021 at 20:03):

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

Mario Carneiro (May 02 2021 at 20:04):

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

Mac (May 02 2021 at 20:04):

That is sufficient structure.

Mac (May 02 2021 at 20:04):

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

Mario Carneiro (May 02 2021 at 20:05):

Okay but then you can't prove anything about it

Mario Carneiro (May 02 2021 at 20:05):

your earlier example had loads of assumptions about the logic

Mario Carneiro (May 02 2021 at 20:05):

I'm using those assumptions, more or less

Mac (May 02 2021 at 20:05):

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 (May 02 2021 at 20:05):

yes

Mario Carneiro (May 02 2021 at 20:06):

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

Mac (May 02 2021 at 20:06):

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

Mac (May 02 2021 at 20:06):

So it is trivially consistent

Mario Carneiro (May 02 2021 at 20:06):

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

Mario Carneiro (May 02 2021 at 20:06):

which is the nearest equivalent to inconsistency

Mac (May 02 2021 at 20:07):

Yes, if you add that to axiom list

Mario Carneiro (May 02 2021 at 20:07):

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 (May 02 2021 at 20:08):

and the converse is trivial by reflexivity

Mac (May 02 2021 at 20:08):

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

Mario Carneiro (May 02 2021 at 20:08):

eval x = eval y

Mac (May 02 2021 at 20:09):

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

Mario Carneiro (May 02 2021 at 20:09):

the right side equality is equality in Nat

Mario Carneiro (May 02 2021 at 20:09):

there is, it's pretty easy to define

Mac (May 02 2021 at 20:09):

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

Mac (May 02 2021 at 20:10):

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

Mario Carneiro (May 02 2021 at 20:10):

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 (May 02 2021 at 20:10):

i.e.

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

Mario Carneiro (May 02 2021 at 20:11):

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

Mac (May 02 2021 at 20:12):

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

Eric Wieser (May 02 2021 at 20:12):

Mario, your eval is not injective

Notification Bot (May 02 2021 at 21:02):

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


Last updated: Dec 20 2023 at 11:08 UTC