# Can you really prove anything from a contradiction, or is that only restricted to formulas?

Let's assume that A∧¬A is provable. It's easy to see how any proposition is provable from that assumption. But since you can prove anything from a contradiction, can you also prove the proposition that "∧A∧ is a formula"? If a statement about the formal system is true, does that reflect on what that formal system is actually like? And if so, does that mean that A∧¬A ⊢ ∧A∧?

• if the deductive system is typical, then no. Most deductive systems are defined over propositions, further they have no notion of "formula" - that a string is a formula is typically a metalinguistic judgement. Oct 29, 2022 at 19:27
• You have the wrong context. From a contradiction any CONCLUSION will be valid. Valid here does not mean true in reality. Valid simply means the premises cannot be true while the premises are false ---that would be impossible to do. Truth in the real world is a different matter. You cannot use a formula that relies on syntax as a random conclusion because how would it be relevant? That would be a non sequitur. /\A /\ is meaningless in Mathematical logic which is what you are using. The syntax matters. Oct 29, 2022 at 19:29
• @Logikal I don't see how what you said answers the question. Oct 29, 2022 at 19:36
• Yes, it is restricted to formulas and that is not a formula of the language: formulas are specified according to the syntactical rules. The formal concept of derivation is defined for formulas. Oct 29, 2022 at 19:56
• You are mixing formulas of the formal system and statements about the formal system. Oct 29, 2022 at 20:02

A formal logic is generally defined in several parts. First, you have an alphabet of symbols like 'a', 'x', '&', '->' where the symbols are given syntactic categories such as constant, variable, etc. Then you have a set of well-formed formulas (WFFs) over this alphabet. For example:

1. If p is a predicate symbol and F is a constant symbol or variable, then p(F) is a WFF.
2. if P and Q are WFFs, then P&Q is a WFF.

Etc. Then after the notion of a WFF is defined, you define rules of inference which always map a set of WFFs into another WFF. That's the essential bit: a rule of inference can only produce a WFF as output.

When someone says that from a contradiction, you can derive any proposition, what they mean is that the rules of inference allow you to derive any proposition from a contradiction. But the rules of inference can only produce WFFs, there is no rule that can derive something that is not a WFF, so what that means is that any WFF can be derived from a contradiction.

• Thank you for your answer. How does it tie into the fact that we can derive a true statement about the formal system? Does that just have no consequence on what the formal system is actually like? Oct 29, 2022 at 21:07
• @NickDoe, I'm sorry, I don't get what you are asking in that comment. Oct 29, 2022 at 23:55
• Well as you say, any formula is provable from a contradiction. That includes every proposition. So the proposition that "∧A∧ is a formula" is also provable from the contradiction. Does this have no effect on what the formal system is actually like under our assumption? Oct 30, 2022 at 0:36
• @NickDoe, Ah! Yes, I suppose if you created a theory of strings in the formal system, including a notion of which strings were WFFs in the formal system itself, and then you introduced a contradiction, you could derive for any string S the theorem that the string is a WFF. But that theorem would itself be an actual WFF. You couldn't derive something that is not a WFF. Oct 30, 2022 at 2:59