tactics for propositional logic

Stream: new members

[Patrick Thomas]

Is there a subset of propositional logic for which a polynomial time algorithm exists?

[Reid Barton]

There's 2-SAT, but probably not the kind of thing you wanted?

[Kyle Miller]

Answering your original question before you edited it, you can exhaustively check the truth table:

example (p q : Prop) : ((p → q) → p) → p :=
begin
  fin_cases p; fin_cases q; simp,
end

That's exponential in the number of variables.

[Patrick Thomas]

I'm mostly curious about what I might be able to try to implement as a tactic, that might be instructive and useful, even if only in known limited cases.

[Patrick Thomas]

Is there more information about the theories behind each of the existing tactics, in addition to what is in https://leanprover-community.github.io/mathlib_docs/tactics.html ?

[Bryan Gin-ge Chen]

I'd look there and in the module docstring of the actual file where the tactics are implemented (you can get there from the tactic doc page by clicking on "related declarations" and then scrolling up to the top). Otherwise you'll probably have to ask about the specific tactic you're interested in here.

[Patrick Thomas]

What does "finish is complete for propositional logic." mean?

[Patrick Thomas]

Suppose that the proof system is just the simply typed lambda calculus, with implication as the only logical connective. Suppose we encode a set of hypotheses and a goal in it. How would a brute force algorithm use a truth table to return false if no proof term exists, and a proof term if one does exist?

[Patrick Thomas]

Mostly I don't see how to go from a truth table to a proof term.

[Mario Carneiro]

If the proof system is STLC with implication only, then it's not classical propositional logic and a truth table approach will not work. But if you have the rules of classical logic (in particular LEM), then you can basically case split on p = true \/ p = false, substitute for p, and then repeat, case splitting on every propositional atom. Each leaf of the case tree corresponds to a single row of the truth table, so if you can prove all of them (by simplification, e.g. using rewrites like (false -> true) = true), then that is just saying that all rows of the truth table come out true, and you get a proof as a result.

[Patrick Thomas]

Why does the truth table approach not work? Does it have something to do with completeness? Is there a different approach that does work?

[Mario Carneiro]

Intuitionistic logic does not have a finite truth table representation; there are decision procedures (like LJT, implemented in tactic#itauto) but you need other methods. The described method obviously doesn't work because it explicitly requires LEM (the principle p = true \/ p = false is just LEM stated slightly differently), and truth table proving is intrinsically connected to the idea that every proposition has one of a finite number of truth values, which is false in intuitionistic logic

[Patrick Thomas]

I see. Thank you.