Yes, in any formal system, all provable statements follow from the axioms. However, there are many formal systems. Two of the most commonly used ones are Classical Logic and the Calculus of Inductive Constructions.
In Classical Logic, “forall P, P or not P” is an axiom. So, it’s technically provable, but it would be misleading to say that you can prove it without further comment.
In the Calculus of Inductive Constructions (which is an extension of Intuitionistic Logic, if I understand correctly), “forall P, P or not P” is not provable.
So if there’s a non-trival proof of “forall P, P or not P”, it isn’t in either of these formal systems. If you do have one in mind, what formal system (logic) is it in, and what does the proof look like?
Yes, in any formal system, all provable statements follow from the axioms. However, there are many formal systems. Two of the most commonly used ones are Classical Logic and the Calculus of Inductive Constructions.
In Classical Logic, “forall P, P or not P” is an axiom. So, it’s technically provable, but it would be misleading to say that you can prove it without further comment.
In the Calculus of Inductive Constructions (which is an extension of Intuitionistic Logic, if I understand correctly), “forall P, P or not P” is not provable.
So if there’s a non-trival proof of “forall P, P or not P”, it isn’t in either of these formal systems. If you do have one in mind, what formal system (logic) is it in, and what does the proof look like?
There’s a non-trivial proof of “P or not P” for a specific P.