11:57 AM
@user525966 Sorry I don't know what you mean by combine systems. You cannot combine different deductive systems, in the same sense that there is no well-defined notion of combining different games. However, I think you meant to say "combine proofs" or "combine axioms".
To answer that, recalled that I have defined what a theorem means:
20 hours ago, by
user21820 @user525966 Short answer is "yes" Long answer: I might have forgotten to define what is a theorem in the Fitch-style system we have gone through. A
theorem is a assertion/statement that is not under any context whatsoever. For example, in the first example proof
here, there are two lines that are outside all the contexts, and those two are theorems.
Now in a deductive system you may also have axioms, which you are allowed to assert anywhere. I did not want to get to that yet, because we were still at propositional logic. Intuitively, "axiom" is supposed to mean something that you are assuming to be true, and hence it makes sense that we are allowed to assert an axiom anywhere. But if you want to talk about combining axioms it means you want to study logic from the outside, so we can consider any set of axioms, nonsensical or not.
We shall write "S |− Q" to mean "The formal system S proves (generates) the statement Q". We so far have a Fitch-style deductive system for PL (propositional logic), and so we can for example say that ( PL |− A or not A ) and ( PL |− A or ( A implies B ) ).
This definition can be applied to any other deductive system for propositional logic, because any one of them will prove the same statements (even though the proofs may look very different).
Now to add the notion of axioms, for a formal system S for propositional logic we shall write "S+X" to mean the same system plus the set X of axioms, meaning that you can use any statement in X as an axiom (besides the axioms S already has).
For example, it is false that ( PL |− A implies B ), but it is true that ( PL+{not A} |− A implies B ). If you want to be precise, it would be PL+{"not A"} |− "A implies B", but it is conventional to omit quotes if the reader can figure out what is a string and what is not (but when I omit quotes I usually enclose in brackets to make sure it is unambiguous).
Okay now we can talk about combining axioms. If you have two sets X,Y of axioms, then PL+X and PL+Y are compatible formal systems that both extend PL, in the sense that, if you have ( PL+X |− Q ) and ( PL+Y |− R ), then you will trivially get ( PL+X+Y |− Q ) and ( PL+X+Y |− R ).
I think this is what you want, because it says that, if from axioms X you can prove Q, and from axioms Y you can prove R, then from axioms X⋃Y you can prove both Q and R.
The question.
Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?
Examples.
In the current stable version of the Lean Theorem Prover, topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes h...
