0

This feels like a basic question or a misunderstanding, but I'm struggling to identify a simple concept having to do with the provability of an argument or proof.

Imagine you have a proof that is well-reasoned and believed true, but then you discover that one of its underlying premises is actually false. Still valid, but unsound.

That false premise is conjuncted with other true premises to create lemmas, which no longer hold. These faulty lemmas are then conjuncted with other premises and lemmas to create further lemmas that no longer hold, and so on, until the conclusion is reached. Clearly, the conclusion no longer holds either. The conclusion itself might be true, it might be false, but it's definitely false that it holds.

My desire is to track those truth values of whether the various steps hold. The point is that these truth values (of whether the lemmas and conclusion hold) travel through the proof identically as they would through AND gates. And yet you would not say that the lemmas or conclusion themselves are false, it's just false that they hold. This is not implication, because the truth table behaves differently - if a proof is based off of the conjunction of two lemmas, and the first lemma does not hold, you would not argue that the proof is true.

In other words, look at the truth table for our favorite Socrates syllogism:

  • A: Socrates is a man
  • B: All men are mortal
  • C: Therefore, Socrates is mortal
A B A ^ B
T T T
T F F
F T F
F F F

I'm not interested in implication (→) here. I am more curious what A ^ B communicates about C. Not the value of C, but the provability of C. Obviously, if B is false, we have not proven Socrates immortal. But A ^ B does mean something about C that is consistent with the above truth table; something that is not implication. It means that the argument for C does not hold if one or more of its premises are false; that it is false that it holds.

What is this logical concept and what symbol should I choose? Are "provable" and "not provable" ( ⊢ and ⊬ ) the best options? i.e.

A B A ^ B A ^ B ⊢ C i.e.
T T T T A ^ B ⊢ C
T F F F A ^ B ⊬ C
F T F F A ^ B ⊬ C
F F F F A ^ B ⊬ C

?

It certainly doesn't seem I should use does/doesn't imply/entail (→ ↛ ⇒ ⇏ ⊨ ⊭), because their truth tables are incompatible. Like if A^B is false, I can't say that "it is false that A^B implies C", because "False implies C" is literally true according to the implication truth table.

It's like I want a more colloquial sense of "implies" that means "Since A and B are not both true, A^B (False) does not (imply) that C holds." Is there a symbol/term for that?

tunesmith
  • 231
  • 1
    You've just written down the truth table for AND; your logical operation is just tracking whether all of the premises are true. I don't quite understand what you mean by "it's false that it holds," but you might be interested in learning about provability logic: https://en.wikipedia.org/wiki/Provability_logic – Qiaochu Yuan Dec 25 '20 at 08:07
  • The syllogism of your question is valid but not as a propositional argument; you need predicate logic to show its validity. – Mauro ALLEGRANZA Dec 25 '20 at 14:27
  • @MauroALLEGRANZA I read somewhere that "all men are mortal" has sometimes gotten interpreted as an implication "if x is a man, then x is mortal". Predicate logic isn't needed to show the validity of this argument under that interpretation. Also, if we assume the categorical syllogisms from Aristotelian logic as valid, the argument has the form of Darii, and thus holds as valid without needing to reference predicate logic. – Doug Spoonwood Dec 25 '20 at 15:30
  • @DougSpoonwood - and in what way do you "link" that to the 2nd premise: "Socrates is a man" ? In propositional logic it is not the same that "x is a man". – Mauro ALLEGRANZA Dec 25 '20 at 16:27
  • This question is specifically about propositional logic. The sentence "All men are mortal" does not need to be represented with predicate symbols in this case. It is enough that it is interpreted as A, which is either true or false. Then if A and B are both true, A&B is true, and it is true that C is established or proven. But if A is true and B is false, the question is what it says about C. A&B yields false, but the meaning of C is not false. It is not false that Socrates is mortal. However, it is clearly false that C is established or proven. – tunesmith Dec 25 '20 at 20:51
  • @MauroALLEGRANZA The link can occur by substituting "x" with "Socrates". – Doug Spoonwood Dec 26 '20 at 03:05
  • @DougSpoonwood - And thus it is predicate logic: in prop logic there is no substitution of an individual variable with a constant term. – Mauro ALLEGRANZA Dec 26 '20 at 09:57
  • @MauroALLEGRANZA Truth values are constants in propositional logic. I don't understand why you want to prohibit substitution with a constant. Some types of propositional logic have a constant in their axioms. – Doug Spoonwood Dec 27 '20 at 06:24
  • @MauroALLEGRANZA Also, in propositional logic even with truth values in the axioms, variables get substituted with axioms or theorems. Even without any interpretation of truth to those axiom, I think the axioms would have to get regarded as constants instead of as variables. – Doug Spoonwood Dec 27 '20 at 07:12

1 Answers1

4

Proofs are not "true" or "false". They are simply syntactic objects over a given formal system. There are no invalid proofs. A purported proof that is not valid is simply not a proof. Proofs have nothing to do with the truth-values of the statements occurring in them. A proof in classical logic only guarantees that if all the axioms used by the proof are true (under some interpretation) then the conclusion of the proof is also true (under that same interpretation).

If you wish to reason about proofs of false statements over the system in which you are performing your reasoning, you may want to use provability logic, so you can say things like $¬A ∧ ⬜( A ⇒ B )$ meaning "$A$ is false and provably $A$ implies $B$". $ \def\dem{\text{Dem}} $

What you are looking for seems to be "$\dem(P,Q) ≡ P ∧ ⬜(P⇒Q)$" meaning "$P$ is true and provably $P$ implies $Q$" (informally "$P$ demonstrates $Q$"). Its negation is "$¬P ∨ ¬⬜(P⇒Q)$" meaning "either $P$ is false or it is not provable that $P$ implies $Q$".

Thus to say "Since A and B are not both true, A^B (False) does not (imply) that C holds.", we can say "$¬(A∧B)$ and hence $¬\dem(A∧B,C)$. But it does not seem to be of much value to do this...

user21820
  • 57,693
  • 9
  • 98
  • 256
  • Thanks very much! The modal operators may be what I need. It looks like I am wanting to propagate truth values about the proof, so provability logic seems like the right track. I actually also do want to distinguish between "not provable because a premise is false" and "not provable yet". The former statement is stronger. An example of the latter is if part of a purported proof relies on premises that are not verified yet. The value of either is that if a purported proof (an argument) does not hold, it will be easy to follow the path to find the point of contention or lack of verification. – tunesmith Dec 26 '20 at 20:07
  • @tunesmith: There is no way to formalize "not provable yet". Every sentence is either provable or not provable. There is no "yet". It is also incorrect that "¬P" is stronger than "¬⬜P". In particular, any formal system that supports provability logic can prove "¬⊥" but cannot prove "¬⬜⊥" unless it also proves "⊥". – user21820 Dec 26 '20 at 20:15
  • As for tracing for actual mathematical proofs, it is trivial to simply trace through the dependencies of proofs. I cannot see anything gained by having an extra layer of reasoning about provability. – user21820 Dec 26 '20 at 20:18
  • I am using three-valued truth - true, false, unknown. For my purposes, a conclusion that rests on a false premise is different than a conclusion that rests on a premise of unknown truth value. I am seeking the proper language to make that distinction. – tunesmith Dec 26 '20 at 20:35
  • @tunesmith: You're going about this wrong. While 3VL (3-valued logic) has some use, it is useless here. Any statement that you think is meaningful (especially about the real world) is going to have a boolean truth-value, so in fact you cannot use 3VL to capture what you do not know. For example, $A∨¬A$ is always true for any meaningful statement $A$ about reality, but it is not a tautology in 3VL. In plain 3VL, there are not even any tautologies. Provability logic is still your best option, but I am saying that there is surely no benefit in using it than to just trace dependencies. – user21820 Dec 27 '20 at 03:11
  • For example: "Any statement I think is meaningful is going to have a boolean truth value." I think that statement is meaningful, but the truth value of it is in doubt to me. So it has an unknown truth value to me. Using 3VL, if conjuncted with a true premise, its lemma would be only "possibly provable" to me, perhaps ◇. If conjuncted with a false premise, its lemma would be "not provable", perhaps ⊬ or ¬◻. If you succeed in convincing me the statement is true, then if conjuncted with a true premise, its lemma would be either provable or proven, I'm not sure which. – tunesmith Dec 27 '20 at 06:06
  • 1
    @tunesmith: I get the feeling that you have insufficient competency in basic FOL, which is why you are making basic logical errors such as conflating truth with beliefs or justifications. Whether it is true or not has absolutely nothing to do with whether you doubt its truth-value. And just to clarify (although it should have been obvious), I was referring to 100% precise statements or interpretations of them, not ill-defined statements like "this man is tall". (By the way, Russell was incompetent in logic and he eventually admitted that.) – user21820 Dec 27 '20 at 08:51