15:44
@user400188 Indeed @user525966 pointed out, you have to explicitly state the lines the rule is applied to, which is more or less the main reason it is not user-friendly. Apart from that, I really like the fact that anyone who learns to use ProofMood (or any Fitch-style proof checker) will (ironically) no longer need to use any proof checker after that. =)
@famesyasd I'm not sure what you now know about the incompleteness theorem, but I recommend you first make sure you grasp everything in my post (linked on the right) up to the explicit independent sentence. That covers the proof-theoretic aspect, namely the lack of a syntactic derivation of some arithmetical sentence (or sentence about programs) and its negation. That's also why it's called syntactic-incompleteness.
The model-theoretic aspect comes via the semantic-completeness theorem (for which you should understand Henkin's proof completely). This fact immediately yields: Given Q independent over S, Q+S has a model and Q+¬S has a model.
When you understand Henkin's proof, you can mentally unfold it to see why there is no issue with S+¬Q having a model, because the model is just some crazy thing built simply to 'evade contradiction', and has nothing to do with the real natural numbers.
Oops, it should be S+Q and S+¬Q...
