Decisions

Q: Are PredicateVariables without SubjectVariable s a kind of PropositionVariable s???
A: Yes, but we only use PredicateVariables with SubjectVariable s. 

Q: Why is the length of an integer restricted. Couldn't BigDecimal be used?
A: In proofs there are several occasions where a (int) position is adressed (proof line number, occurence, ...). To avoid problems at this stage, integer values are restricted generally to (positive) int values.

Q: Why is quantifing over a formula that hasn't x as a bound variable forbidden if x is no free variable?