Metamathematics in lean 4

Stream: Type theory

[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

[Mario Carneiro]

it's not supposed to be

[Mac]

Mac said:

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

But that isomorphism does exist organically.

[Mario Carneiro]

it's supposed to translate L-provably equal terms into equal natural numbers

[Mario Carneiro]

Mac said:

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

Not obviously: That only holds for the decidable fragment. If I use PA in place of L, then that will not be true for many quantified statements

[Mario Carneiro]

for example PA |- Con(PA) is false but Con(PA) is true (in lean)

[Mac]

I meant the PA fragment we were discussing.

[Mario Carneiro]

Without quantifiers, the logic becomes a roundabout way of talking about Nat

[Mario Carneiro]

that was my point

[Mac]

Okay, and that is a problem why?

[Mario Carneiro]

well, L doesn't contribute much in that case

[Mac]

well it is more limited than Nat

[Mac]

At least my fragment is

[Mario Carneiro]

Does your fragment have the axioms needed to establish the theorem I mentioned?

[Mac]

For example with my semiring fragment you can't prove 0 = 1 or 0 \ne 1

[Mario Carneiro]

but you can prove that 0 = 1 -> x = y

[Mario Carneiro]

which seems like basically the same as 0 \ne 1

[Mac]

Mario Carneiro said:

but you can prove that 0 = 1 -> x = y

How?

[Mac]

You can only prove that (L |- x = y) -> (eval x = eval y) for your eval

[Mac]

You can't prove eval x = eval y -> (L |- x = y)

[Mario Carneiro]

That should be the easy direction

[Mac]

My fragment lacks reflexivity

[Mario Carneiro]

ah... what

[Mario Carneiro]

ok then

[Mario Carneiro]

do you have 0 = 0?

[Mac]

no

[Mac]

That is not necessary for the semiring proofs

[Mario Carneiro]

do you have symmetry and transitivity?

[Mario Carneiro]

and 0 + 0 = 0

[Mac]

only transitivity and left euclideanness

[Mario Carneiro]

left euclidean implies transitive and symmetric

[Mac]

no it does not.

[Mac]

transitive and symmetric does imply left euclidean though

[Mario Carneiro]

do you have x + 0 = x?

[Mac]

yes

[Mario Carneiro]

then by left euclidean you have reflexivity

[Mac]

How?

[Mario Carneiro]

x + 0 = x and x + 0 = x so x = x

[Mac]

left euclidean, not right euclidean

[Mac]

x + 0 = x and x + 0 = x so x + 0 = x + 0

[Mac]

Furthermore, even if I had (L |- x = y) <-> eval x = eval y that does not prove that (L |- ~(x \ne y)) <-> (eval x \ne eval y), right or even ((L |- x = y) -> False) <-> ((eval x = eval y) -> False) (because Lean is intuitionistic)?

[Mario Carneiro]

Nat equality is decidable (also Lean is pretty classical)

[Mario Carneiro]

the last one is just not_congr applied to the first

[Mac]

Mario Carneiro said:

the last one is just not_congr applied to the first

Ah, but does it matter that (L |- x = y) is not necessarily a prop?

[Mario Carneiro]

not really, except that <-> doesn't apply to non-props

[Mario Carneiro]

just substitute L |- p = q with nonempty (L |- p = q)

[Mac]

Also, now that I think about it how do you even get (L |- x = y) -> eval x = eval y

[Mac]

how do you get from (L |- 0 = 0) to eval 0 = eval 0?

[Mario Carneiro]

That was the argument by inconsistency I mentioned

[Mario Carneiro]

That one is easy, ignore the proof

[Mario Carneiro]

0 = 0 is true

[Mac]

Oops, dumb me XD

[Mac]

how do you get from (L |- S 0 = 1) to eval (S 0) = eval 1

[Mario Carneiro]

That one is also true

[Mario Carneiro]

it's true by rfl

[Mac]

How so?

[Mario Carneiro]

This is where eric's observation that eval is not injective comes in

[Mac]

Remember that 0, S, and 1 are members of some arbitrary type P

[Mac]

sure, you gave an example of eval for one possible P

[Mac]

But you would need an eval instance of every possible type P

[Mac]

that has 0, S, and 1 instances

[Mario Carneiro]

In that generality it requires more assumptions: specifically, it only holds for terms built from 0, S, 1, and only if 0, S, 1 are distinct

[Mac]

what "it" requires more assumptions?

[Mac]

eval?

[Mario Carneiro]

In order to define eval, you need those assumptions

[Mario Carneiro]

and the theorem about eval that I mentioned only holds on those terms

[Mac]

So, i.e. the point of L

[Mario Carneiro]

If there are weird extra terms then you don't know whether they are equal or not

[Mario Carneiro]

unless there is an induction principle

[Mac]

exactly

[Mario Carneiro]

the induction principle lets you prove that there are no weird extra terms

[Mac]

So now eval has become almost as complex as L (and maybe more so)?

[Mac]

I again am missing your point.

[Mario Carneiro]

eval is exactly as complex as L, it's a function defined on L

[Mac]

so what was the point of this whole endeavor?

[Mario Carneiro]

if the theory is decidable then it is nice to have a decision procedure

[Mario Carneiro]

eval x = eval y is a decision procedure

[Mac]

But as we have already pointed out my fragment of PA is not decidable

[Mario Carneiro]

I'm not sure that's true

[Mac]

for one, it lacks reflexivity

[Mario Carneiro]

your fragment is perhaps not as simple as I said but that doesn't mean it's not decidable

[Mario Carneiro]

I would actually be surprised if it's not decidable

[Mac]

I mean I can't decide if (L |- 0 = 0) is true or false, that makes L undecidable, right?

[Mario Carneiro]

(I'm not entirely sure this is true, but) assuming that there is no hidden extra way to prove 0 = 0, then L |- 0 = 0 is false and hence decidable

[Mario Carneiro]

the goal here is to decide whether L |- x = y is true or false given terms x, y

[Mac]

I also can not prove (L |- 0 = 0) -> False either.

[Mac]

After all, Lean is not complete, right?

[Mario Carneiro]

I would be extremely surprised if it is actually independent of lean

[Mac]

How would I prove that?

[Mac]

None of the axioms provide me with a way to get false. I have no knowledge of the structure of L or P to do a proof by cases.

[Mario Carneiro]

You do have to assume that there are no additional axioms beyond the ones enumerated

[Mac]

So I would assume that (L |- 0 = 0) and (L |- 0 = 0) -> False are both not provable from the PA fragment

[Mario Carneiro]

I am saying that the PA fragment does not prove 0 = 0

[Mac]

Mario Carneiro said:

You do have to assume that there are no additional axioms beyond the ones enumerated

Ah, well then yes, (L |- 0 = 0) -> False is trivially provable.

[Mario Carneiro]

Not trivially, I think

[Mac]

By trivially. I meant under the current assumption that (L |- 0 = 0) is not an entailment of the fragment

[Mac]

Proving it might not be so fun.

[Mario Carneiro]

So the thing that is being proven in lean is really not ((L : Logic) -> (assumptions) -> (L |- 0 = 0))

[Mac]

Logic would have to a minimal representation of assumptions to show that though.

[Mario Carneiro]

and the proof is that if you take L to be the minimal logic satisfying the assumptions, then you can disprove L |- 0 = 0

[Mac]

i.e. you would also need an hypothesis stating that.

[Mario Carneiro]

so therefore it is not the case that every logic satisfying the assumptions has L |- 0 = 0

[Mac]

Mario Carneiro said:

and the proof is that if you take L to be the minimal logic satisfying the assumptions, then you can disprove L |- 0 = 0

correct

[Mario Carneiro]

you don't need minimality to be part of the theorem statement

[Mac]

So this maybe: exists (L : Logic) => not ((assumptions) -> (L |- 0 = 0))?

[Mario Carneiro]

yes, that's equivalent

[Mario Carneiro]

Do you mind if I relocate this conversation to #Type theory ? It's not a perfect fit but I feel like this has gotten somewhat off topic for the lean 4 stream

[Mac]

sure feel free

[Notification Bot]

This topic was moved here from #lean4 > associativity of ↔ by Mario Carneiro

[Mac]

though I might be more inclined to put it in the more general #maths instead (since that is one of the default streams)

[Mario Carneiro]

well I'm also concerned about putting hundreds of messages in everyone's inbox for a conversation that is mostly just us

[Mario Carneiro]

I don't think there are too many folks who do mathematical logic around here

[Mac]

Mario Carneiro said:

I don't think there are too many folks who do mathematical logic around here

That surprises me.

[Mario Carneiro]

mathlib doesn't really have any definition of a logic; the closest analogue is the definition of logic in flypitch (which was needed in order to state and prove the independence of CH)

[Mario Carneiro]

There are a few individual projects that have defined logics, but they are mostly one-off projects. I think Minchao Wu has a definition of a modal logic, as well as Paula Neeley; Alexandre Rademaker has some ontology thing that I don't fully understand; and there have been a few definitions of lambda calculus (with or without types) in this stream

[Mario Carneiro]

By the way, check out https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/Modelling.20a.20Type.20Theory.20in.20Lean/near/202076965 ; and_to_imp is the implication introduction rule I mentioned, although in this version G is just a single formula connected by conjunctions instead of a list

[Mac]

I still think my conditional proof rule is fine for the general case (and it mirrors the elimination rule, which is nice). It works fine in complete logics (such as propositional and first-order), so I will probably leave it as is. May introduce a more restrained version later. I would also argue that the restrained version is just relevant logic implication then (and, as such, I may touch on it if I end up spending some time formalizing that).

[Mac]

I also don't generally end up using the propositional logic rules in my proofs because I can generally leave that to the metalogic (as I did in my PA fragment).

[Mac]

i.e. PProd (L |- p) (L |- q) is just as good as (L |- p /\ q) and (outside of classical logic) PSum (L |- p) (L |- q) is often just as good as L |- p \/ q

[Mario Carneiro]

I still think my conditional proof rule is fine for the general case (and it mirrors the elimination rule, which is nice). It works fine in complete logics (such as propositional and first-order), so I will probably leave it as is.

The fact that it's not well founded should make it very suspicious as a proof rule. It's a constraint on the provability judgment that is not satisfiable like a standard axiom rule

[Mac]

What is wrong with it not being well-founded?

[Mario Carneiro]

it sort of fails the concept that a theory is inductively generated by axioms and rules of inference

[Mac]

I wonder what you would think of this variation of the natural induction rule then:

(f : T -> Sort w) -> f 0 ->
    ((n : T) -> (L |- nat n) -> (f n -> f (S n))) ->
    ((n : T) -> (L |- nat n) -> f n)

[Mario Carneiro]

Oh, I can definitely use that to prove nonsense

[Mario Carneiro]

That axiom implies that all terms are syntactically of the form S S S ... S 0, so 1 doesn't exist

[Mac]

I'd love to see it. I figured as much, but I have yet to see any pitfalls. Maybe I'm just not that creative.

[Mario Carneiro]

well, I guess it's fine if the term language isn't really a term language and is really Nat

[Mac]

Mario Carneiro said:

That axiom implies that all terms are syntactically of the form S S S ... S 0, so 1 doesn't exist

How does it imply that?

[Mac]

It does have the (L |- nat n) constraint for n

[Mario Carneiro]

you take f to be the assertion that n = S^i 0 for some i : Nat

[Mario Carneiro]

Mac said:

It does have the (L |- nat n) constraint for n

That's true, I really only mean that L |- nat n implies n = S^i 0 for some i

[Mac]

Isn't that generally true?

[Mario Carneiro]

= here is lean's Eq, i.e. syntactic equality

[Mario Carneiro]

If T is a term language containing things like 0 + 0 or 1 then that would usually not be true

[Mario Carneiro]

in particular you can probably use this to prove reflexivity

[Mac]

Also how would you show n = S^i 0?

[Mac]

ah I see.

[Mac]

I don't actually use this prove the Peano fragment though, luckily.

[Mac]

I use this:

(C : T -> T -> P) -> (f : T -> T -> T -> P) ->
    ((a b : T) -> (L |- nat a) -> (L |- nat b) ->
      (L |- C a b) -> (L |- f a b 0)) ->
    ((c : T) -> (L |- nat c) ->
      ((a b : T) -> (L |- nat a) -> (L |- nat b) ->
        (L |- C a b) -> (L |- f a b c)) ->
      ((a b : T) -> (L |- nat a) -> (L |- nat b) ->
        (L |- C a b) -> (L |- f a b (S c)))) ->
    ((a b c : T) -> (L |- nat a) -> (L |- nat b) -> (L |- nat c) ->
      (L |- C a b) -> (L |- f a b c))

[Mac]

and this:

(f : T -> T -> T -> P) ->
    ((a b : T) -> (L |- nat a) -> (L |- nat b) ->
      (L |- f a b 0)) ->
    ((c : T) -> (L |- nat c) ->
      ((a b : T) -> (L |- nat a) -> (L |- nat b) -> (L |- f a b c)) ->
      ((a b : T) -> (L |- nat a) -> (L |- nat b) -> (L |- f a b (S c)))) ->
    ((a b c : T) -> (L |- nat a) -> (L |- nat b) -> (L |- nat c) ->
      (L |- f a b c))

[Mac]

Also, considering how quickly you poked a hole in that natural induction rule, I'm curious as to whether you think there is also a problem with this disjunction elimination rule:

(p q : P) -> (L |- p \/ q) ->
    (r : Sort w) -> ((L |- p) -> r) -> ((L |- q) -> r) -> r

[Mario Carneiro]

That one also implies that the theory is complete, if it satisfies excluded middle

[Mac]

I guess a better question is, is it any worse than:

(p q : P) -> (L |- p \/ q) ->
    (r : P) -> ((L |- p) -> (L |- r)) -> ((L |- q) -> (L |- r)) -> (L |- r)

[Mac]

Since, yeah, I keep the metalogic (L |- p) -> (L |- q) as entailment throughout.

[Mac]

Which I still think is reasonable.

[Mario Carneiro]

Why not just have axioms like (L |- p \/ q) <-> (L |- p) \/ (L |- q), (L |- p -> q) <-> ((L |- p) -> (L |- q)) and so on, if you want metalogical connectives

[Mac]

Because (L |- p) is not a prop and <-> is not function.

[Mario Carneiro]

insert nonempty everywhere

[Mac]

The point is to reduce complexity, not increase it. XD

[Mario Carneiro]

I'm not sure why |- isn't a prop though

[Mac]

Also, a proof my depend on only one direction of the rule.

[Mac]

|- is not a prop so that a judgment can potential be an inductive type which one can do proof by cases on.

[Mario Carneiro]

it can still be an inductive prop

[Mario Carneiro]

you can do proof by cases on an inductive prop

[Mac]

And for cases where I want type safety from Props.

[Mario Carneiro]

type safety?

[Mac]

Mario Carneiro said:

you can do proof by cases on an inductive prop

Doesn't that violate proof irrelevance?

[Mario Carneiro]

Proof by cases to prove a proposition

[Mac]

I guess my point is: I am trying to avoid proof irrelevance.

[Mario Carneiro]

you don't need to use proof irrelevance

[Mario Carneiro]

but AFAICT your theory is not really changed at all by putting everything in prop

[Mac]

If (L |- p) : Prop then for all p1 p2 : L |- p , p1 = p2 by proof irrelevance, correct?

[Mario Carneiro]

yes

[Mac]

That's what I don't want

[Mario Carneiro]

You can just have Derivation L p and define L |- p = nonempty (Derivation L p)

[Mario Carneiro]

which matches conventional usage better anyway

[Mac]

but L |- p is suppose to be the proof type not a proposition that there is a proof.

[Mario Carneiro]

so L |- p means p is provable and Derivation L p is the type of proofs of p

[Mac]

By (L |- p) -> (L |- q) I mean given a proof in L of p I can construct a proof in L of q which is the result of this function.

[Mario Carneiro]

lean is classical so that doesn't really mean as much as you want it to

[Mac]

Lean is not classical

[Mario Carneiro]

sure it is, Classical.em is a thing

[Mac]

yes, but that adds axioms to proof

[Mario Carneiro]

and the core tactics don't particularly shy away from it

[Mac]

Hence why I am avoiding the core

[Mario Carneiro]

If you are working in an intuitionistic metatheory then things are different, but I think lean isn't the best choice for that

[Mac]

Why not? And what do you think would be a better place?

[Mario Carneiro]

I'm mostly assuming that you are comfortable with assuming classical logic and countably many inaccessible cardinals (in the metatheory) because lean is kind of hostile to not assuming that

[Mac]

Also I use Lean primarily for its metaprogramming power, not its logical base.

[Mario Carneiro]

You can restrict the object logic if you want to, but you have to be careful not to let the excessively strong metalogic bleed into the object logic

[Mac]

Mario Carneiro said:

You can restrict the object logic if you want to, but you have to be careful not to let the excessively strong metalogic bleed into the object logic

Very true.

[Mario Carneiro]

which means things like (L |- p) -> (L |- q) are problematic

[Mario Carneiro]

because that's Lean's function space, not the object logic's

[Mario Carneiro]

who knows what crazy things are in there

[Mac]

True, I understand that. I am using it mostly for ease of use.

[Mac]

Otherwise I would have to create some alternative syntax to do proofs in, which I am not quite ready to do yet.

[Mario Carneiro]

have you considered using a hilbert style axiomatization? That avoids the need for a context in the provability judgment

[Mac]

One of the key parts of logics in my metalogic is that they are initially devoid of both inference rules and syntaxes. Rules and syntax are part of the hypotheses of proofs.

[Mario Carneiro]

I mean as hypotheses

[Mario Carneiro]

that is, you can assume L |- p -> p and L |- (p -> (q -> r)) -> (p -> q) -> p -> r and such

[Mario Carneiro]

I think it would be easier to bundle them into sets though

[Mac]

Yes, but most proofs ideally operate in heavily constrained logics (as my Peano proofs did). They don't generally even have any propositional logic at all.

[Mac]

So the goal is not to minimize the axiomization (but in many cases, to maximize it).

[Mario Carneiro]

I've heard of an axiomatization of primitive recursive arithmetic that doesn't use any logical connectives, only inference rules and =

[Mario Carneiro]

oh, it's on wiki: https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic#Logic-free_calculus

[Mac]

I believe that if I wanted to better constrain Lean from bleeding into my proofs, I would have construct a restricted logic within Lean and then construct my metalogic system within that restricted logic.

[Mac]

I am not really sure I want to do that yet.

[Mario Carneiro]

It kind of sounds like you want LF

[Mario Carneiro]

Or possibly MM0, although I'm pretty scared to suggest my language to anyone. But it was designed for use cases roughly like this

[Mario Carneiro]

What kind of automation are you using from lean 4?

[Mac]

My big draw to Lean is its metaprogramming power (namely its customizable syntax).

[Mario Carneiro]

Is it just notations like L |- p and x = y? Because that's not hard to find

[Mario Carneiro]

would lean 3 satisfy your notational needs?

[Mac]

Also things like forall and exists, but yeah, for this project its probably not that much.

[Mac]

Lean 3's problem is that it has to many reserved notations (which tends to be a problem in a lot of languages).

[Mac]

Though, yeah, initially started in Lean 3 before moving to Lean 4, so I don't think it'd be impossible.

[Mac]

Though I do value the easy of use of Lean 4 (and the syntax highlighting of custom notation).

[Mario Carneiro]

Interesting. You might actually like MM0 then, it is kind of like lean but you define the entire theory yourself; generally it's some kind of FOL but you get to pick all the axioms, notations and so on

[Mac]

You really should get some github syntax highlighting for it :)

[Mario Carneiro]

You need to have X number of users before github will care about you

[Mario Carneiro]

I checked

[Mario Carneiro]

it would be great if they had repo-specific highlighting but I guess that's some kind of security concern

[Mac]

also, what is with all the $

[Mario Carneiro]

just pretend it's latex

[Mario Carneiro]

it is to prevent weird mathematical notation from corrupting the "outer" syntax

[Mario Carneiro]

inside the $ you can have whatever you like

[Mac]

why?

[Mac]

why not just use braces for definitions then?

[Mario Carneiro]

I don't follow

[Mac]

i.e. { ... } instead of = $ .. $ (or : $ ... $

[Mario Carneiro]

The $ delimit user-defined mathematical notation sections

[Mario Carneiro]

It could be { ... } but then that would limit the use of { ... } inside mathematical notation

[Mac]

yes but in https://github.com/digama0/mm0/blob/master/examples/x86.mm0, virtually every definition is within $s

[Mario Carneiro]

yes, they are mandatory

[Mario Carneiro]

Inside the $ you can use literally any character, keyword, whatever

[Mac]

my point is why not instead of

def bit (n i: nat): nat = $ nat (i e. n) $;
theorem bitT (n i: nat): $ bool (bit n i) $;

having:

def bit (n i: nat): nat { nat (i e. n) }
theorem bitT (n i: nat): bool (bit n i)

[Mac]

were the colon consume math notation until the end-of-line

[Mario Carneiro]

because newlines are permitted in math strings

[Mac]

in which case you use braces instead

[Mario Carneiro]

and semicolons

[Mario Carneiro]

and braces

[Mario Carneiro]

and unmatched braces

[Mario Carneiro]

arguably that's too permissive

[Mac]

okay, ignore the colon sugar, here is also a possibility:

def bit (n i: nat): nat { nat (i e. n) }
theorem bitT (n i: nat) {  bool (bit n i) }

[Mac]

Yeah the unmatched braces seem a bit of a stretch.

[Mac]

However, why not run a custom parser?

[Mac]

like Lean 4 does?

[Mario Carneiro]

Because MM0 is designed to be simple to parse

[Mario Carneiro]

lean 4 is... not

[Mac]

Mario Carneiro said:

lean 4 is... not

In one manner of speaking yes, In another manner of speaking, no

[Mac]

Lean actually has a pretty simple parsing algorithm (outside of anti-quotes)

[Mario Carneiro]

I'm not sure how to interpret that to make it true. Lean has an extremely extensible parsing system, which has been extended already in the core quite a bit to build the core syntax

[Mac]

As a person who has long been toying with a writing a metaprogramming language with the parsing flexibility of Lean (and beyond), I am actually amazed at how they were able to write such a flexible parser with such simple rules.

[Mac]

Yes but the core is surprisingly simple for being so flexible.

[Mario Carneiro]

sure, but in order to actually parse things you need all the extensions too

[Mac]

Yes, but the extensions are written in Lean, so that is less of a problem.

[Mac]

So as long as you can parse the basics, you can parse the more complex cases by interpreting the basics.

[Mario Carneiro]

It has to be staged though, notations are used before they are defined

[Mac]

true

[Mario Carneiro]

I went for more the opposite approach, what's the simplest extensible parser that can be used to define not terrible looking formal maths

[Mario Carneiro]

and can be specified in a page or two

[Mac]

which I applaud, as the result looks quite good

[Mario Carneiro]

the dollar delimiters are so that the outer syntax parser can be a fully static parser like what yacc gives you

[Mario Carneiro]

although it doesn't have to be implemented that way

[Mac]

However, I must admit it does offend my sensibilities somewhat.

[Mac]

I suspect that means the syntax highlighting leaves much to be desired.

[Mario Carneiro]

I'll find a nice subdued color for the syntax highlighter :)

[Mario Carneiro]

there is an online tutorial video which shows the syntax highlighting

[Mario Carneiro]

but the dollars are just white

[Mac]

How does it highlight the bits of notation within the dollars?

[Mario Carneiro]

right now it doesn't. The regex highlighter isn't smart enough to know the user notation

[Mac]

that was my point

[Mario Carneiro]

but I am planning to add "semantic highlighting" messages from the server, which would allow various kinds of highlighting, although I'm not sure what to do besides highlighting the variables

[Mario Carneiro]

to be fair, lean doesn't do any math highlighting either

[Mac]

One of the things love about Lean's syntax highlighting is that custom keywords (ex. forall) get highlighted the same as builtin keywords.

[Mario Carneiro]

heh that's a bug

[Mac]

what makes you say that?

[Mario Carneiro]

forall is a lean keyword

[Mac]

I know, I was just using that as an example

[Mac]

As I can't quite give an common example of a custom keyword, can I?

[Mario Carneiro]

Actually you are right, there is an actual feature along those lines. There was a bug like that in lean 3 for a while though

[Mac]

I presumed it was feature, as it isn't in 4.0.0-m2 but it is in the nightly so it must have been added recently.

[Mario Carneiro]

For example the obtain tactic was nicely highlighted, not because the highlighter knew that obtain was a tactic, but because obtain was a keyword in lean 2 and the highlighter was never updated

[Mac]

Obviously none of this occurs on Github :(

[Mario Carneiro]

But you are right, if you define a custom tactic in lean 4 it will get highlighted using the "semantic highlighting" feature

[Mac]

I love that. It makes custom notation feel natural as opposed to a wart you glued onto the system.

[Mario Carneiro]

you can tell because it takes a little bit of extra time to get highlighted compared to the rest of the text

[Mac]

Exactly! XD

[Mario Carneiro]

I think variable highlighting is another way to give the text a little more texture

[Mario Carneiro]

I wouldn't know how to start highlighting user notations though

[Mac]

I am said that most color schemes and highlighters have gotten rid of operator highlighting. I quite liked that.

[Mac]

Mac said:

I wonder what you would think of this variation of the natural induction rule then:

(f : T -> Sort w) -> f 0 ->
    ((n : T) -> (L |- nat n) -> (f n -> f (S n))) ->
    ((n : T) -> (L |- nat n) -> f n)

Something I was curious about: Is there a clean way of restricting f to judgments or functions of judgments (since they are both just Sorts)?

[Mario Carneiro]

Even with the judgment version, I think it wouldn't be sufficient, since you can still let f be if \exists i, n = S^i 0 then term.true else term.false as long as the proposition language contains something true and something false

[Mario Carneiro]

but to answer your question, yes you can make an inductive type out of this

[Mac]

Mario Carneiro said:

but to answer your question, yes you can make an inductive type out of this

Yeah, but that's a different type then.

[Mario Carneiro]

I mean you can have a predicate on functions f meaning "f is a judgment or function of judgments"

[Mac]

Now that I think about this, is the exists i, n = S^i 0 that bad? It would expand to this:

(0 = S^i 0) ->
((n : T) -> (L |- nat n) -> ((exists i, n = S^i 0) -> (exists i, S n = S^i 0)) ->
((n : T) -> (L |- nat n) -> (exists i, n = S^i 0))

This is what natural induction means right: that every nat is 0 or a S of a nat?

[Mac]

It is certainly stronger than my current PA fragment, but it seems pretty standard for arithmetic

[Mario Carneiro]

well, like I said, if T is a type of terms, such that 0 + 0 and 0 are not equal in the lean sense, then this property will fail because 0 + 0 is not of the form S^i 0

[Mario Carneiro]

take note that the assumption is not L |- n = S^i 0 but n = S^i 0

[Mac]

true, but that makes sense, considering this is metalogical object-nat induction rather than object logic nat induction.

[Mario Carneiro]

Right, so this can be used to prove that the object nats are really the metalogic nats

[Mac]

makes sense.

[Mac]

in essence, this is a way of encoding that property.

[Mario Carneiro]

which can then be used to prove other things like reflexivity or Con(PA)

[Mac]

I forgot, what does Con(PA) denoted again?

[Mario Carneiro]

PA Is consistent

[Mac]

ah, should have guessed that.

[Mario Carneiro]

indeed Con(ZFC) can probably be smuggled in too

[Mario Carneiro]

essentially L will look like "true arithmetic" from lean's point of view, so all true (that is, lean-provable) nat facts become L facts

[Mac]

this induction is thus structural induction for nats opposed to equality-based induction for nats

[Mac]

Mario Carneiro said:

essentially L will look like "true arithmetic" from lean's point of view, so all true (that is, lean-provable) nat facts become L facts

isn't it that opposite, all L nat facts become Lean nat facts?

[Mario Carneiro]

it's both, to the extent that L models negative nat facts

[Mac]

Wait a second does this even prove L |- 0 = 0?

[Mac]

all that equality proof tells me is the structure of nat terms, it doesn't give me properties about them.

[Mario Carneiro]

The argument is roughly that since L |- 0 + 0 = 0, it suffices to prove 0 + 0 = 0. By the induction lemma 0 + 0 = S^i 0 so it is either 0 or 0 + 0 = S x; but in this case L |- S x = 0 and I guess this violates some axiom

[Mac]

i.e. it tells me if 3 + 4 is a nat term then it is some successor of zero, it doesn't tell me which one, right?

[Mac]

Mario Carneiro said:

The argument is roughly that since L |- 0 + 0 = 0, it suffices to prove 0 + 0 = 0. By the induction lemma 0 + 0 = S^i 0 so it is either 0 or 0 + 0 = S x; but in this case L |- S x = 0 and I guess this violates some axiom

So as long as I have the S n \ne 0 axiom it does, but without it, it doesn't.

[Mario Carneiro]

I believe it's possible to use that to prove L |- 1 = 0 by taking predecessors of both sides enough times

[Mac]

thing is because this the term 0, 0 itself can still be equal to the successor of some other nonzero (non-nat) number like -1

[Mac]

I believe 0 = (S -1) or the like would still be consistent

[Mario Carneiro]

Oh sorry, by x I actually mean S^i 0

[Mario Carneiro]

that is, in the hypothetical we know that e.g. L |- S S S 0 = 0

[Mario Carneiro]

so it's not -1 unless S is cyclic or something

[Mario Carneiro]

which it might be without the S x != 0 axiom

[Mac]

yeah, that was my point

[Mac]

without the axiom, we have no knowledge of where the ladder starts or stops (or if it does)

[Mac]

I just remembered this, so I'll put this here.
Mario Carneiro said:

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

Mario Carneiro said:

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

First, This is only true if (L |- p -> false) -> (L |- not p)holds (or, more generally, if (L |- p -> q) -> (L |- not p) for some q holds). Furthermore, if the logic lacks the law of excluded middle even at statement like (L |- p <-> not p) is fine. I think you may be under-estimating the number of logics in which this conditional proof rule is fine.

[Mac]

However, I do thank you for bringing to my attention these properties of my conditional proof rule. I probably wouldn't have noticed them myself. So thanks! :smile:

[Mario Carneiro]

@Mac Indeed, as I've said every logical argument I made requires some assumptions on the logic (and it's not too difficult to reverse engineer the required rules from the argument itself, in reverse mathematics style). You can't get anywhere if you don't make any assumptions at all. But just because the argument fails if the logic is so impoverished that p -> false and not p are not equivalent doesn't mean it's a good proof rule, because at the very least it means you have an "anti-establishment" proof rule that is incompatible with the traditional axioms you would find in a mainstream theory like PA or ZFC. Usually, when doing this kind of theory exploration, the rules are supposed to be at least compatible with what traditional FOL does, and I am trying to show how it is not. So you are exploring some other incompatible island in theory space, which might be interesting, but probably is less applicable than you thought.

[Mac]

@Mario Carneiro That 's fair. Thanks again!

[Mac]

One thing I'm still curious about though, is why do most standard mathematical logics embedded the logic with the math. What particular pitfalls does relegated logical connectives to the metalogic and leaving only the mathematical predicates and numbers (equality, numbers, sets, etc.) to the object logic create?

[Mario Carneiro]

That sort of thing is often known as higher order abstract syntax (HOAS) in the biz. It works pretty well in LF, but it requires that the metatheory be very weak, so that function types correspond roughly to things that can be represented by terms in the logic

[Mario Carneiro]

for example, you would generally want the function type in such a system to be countable and satisfy a paremetricity metatheorem

[Mario Carneiro]

If the metatheory is sufficiently advanced so as to be able to do general mathematics, the function type will be uncountable and contain "wild" terms in it which break parametricity. HOAS is usually inconsistent in such systems, and Lean falls in this category

[Mario Carneiro]

The paper Higher Order Abstract Syntax in Coq discusses some of the difficulties of implementing HOAS in Coq, which has similar issues to Lean (Lean has it a bit worse because classical logic admits even more exotic terms than plain old DTT)