channel for formalizing classical logic

Stream: general

[Paige Thomas]

Would it be possible to have a channel devoted to formalizing classical logic in Lean?

[Shreyas Srinivas]

Isn’t there a huge repo with godel’s incompleteness theorems already on its way up to mathlib?

[Matt Diamond]

Yes and no... there is a huge logic formalization repo:
https://github.com/FormalizedFormalLogic/Foundation

However, it appears that there are currently no plans to port it to Mathlib:
https://github.com/orgs/FormalizedFormalLogic/discussions/159

[Junyan Xu]

See also #general > Discussion: FormalizedFormalLogic @ 💬

[Paige Thomas]

I was mostly thinking of just a place to organize the questions I run into studying and formalizing classical logic. It's not really intended to go into Mathlib. Currently I've started working my way through "Handbook of Practical Logic and Automated Reasoning" by John Harrison and formalizing parts from it. One eventual goal is to have a proof assistant for classical logic with a core checker formalized in Lean, which @Mario Carneiro has helped me achieve a great deal of progress on. But I just meant the channel as a place to organize questions about classical logic in general and, or formalizing it in Lean. It might not get a lot of use, I don't know, no problem if nobody wants it.

[Paige Thomas]

(deleted)

[Luigi Massacci]

I think you’ll just be better off with using #new members, as well as #lean4 and #metaprogramming / tactics for that

[Luigi Massacci]

also, if you like the syntactic side of logic and are looking for a project, I was amazed to discover that tauto just uses solve_by_elim, and is practically begging to be rewritten into a proper decision procedure (whether using the LJT calculus so it can be more straightforwardly lifted from Coq, or one of the more modern sequent calculi)

[Mario Carneiro]

@Luigi Massacci tauto via LJT is already implemented, that's itauto

[Mario Carneiro]

we could probably replace tauto with itauto! and maybe no one will notice? There is the issue that itauto is more strict about only solving propositional logic goals, while tauto is okay with some light predicate logic as well

[Luigi Massacci]

I see I should have scrolled further up the documentation :man_facepalming: Maybe instead of replacing tauto with itauto!, it could call the latter if the current approach fails? I would imagine the brute force-ish strategy is precisely what helps with the predicate stuff.

[Vasilii Nesterov]

Luigi Massacci said:

also, if you like the syntactic side of logic and are looking for a project, I was amazed to discover that tauto just uses solve_by_elim, and is practically begging to be rewritten into a proper decision procedure (whether using the LJT calculus so it can be more straightforwardly lifted from Coq, or one of the more modern sequent calculi)

I'm probably late to the party, but what's wrong with the current tauto implementation? It looks like a decision procedure for propositional logic to me.

[Vasilii Nesterov]

(except that it can be very slow, which is rare in practice)

[Luigi Massacci]

The "proper" was meant in the moral sense of the word ; ) I guess it should be complete since solve_by_elim does IDDFS, but it applies lemmas greedily, which is really sub-optimal