Well for one, your two examples aren't "true".
Fix a language (may it be first order language of English), and consider any property . Classically, we take the law of excluded middle (LEM) as axiom so that for any such property,
holds.
Now take any predicate , and for any , the claim says that the property either holds for it or not. And indeed, by LEM, we have
If you adopt a mathematics with this sort of rule, then you force a non-constructive interpretation on the subject, because we can (as we know since Turing) come up with predicates that can't be evaluated by humans. E.g. the mortal matrix problem
>Given two arbitrary 15-by-15 matrices A,B with integer entries, can they be multiplied in some way, possibly with repetition, such that they give the zero matrix.I.e. naively you'd start trying out
>A, B, AB, BA, ABA, ... ABBBABAABAAA,... and this makes for a word problem that Emil Post and those early CS guys have shown is such that there can't possibly be a clever algorithm that is able to, for any given two such matrices, correctly compute whether they can be multiplied to a zero matrix.
https://en.wikipedia.org/wiki/List_of_undecidable_problemsYou can be an ultrafinitists or at least a hard formalists like the Russian school, but even they considered e.g.
https://en.wikipedia.org/wiki/Markov%27s_principleAs far as axioms are concerned to which you can easily find models (e.g. the axiom of groups, where 0, 1 and addition mod 2 is a first model), then those axioms are mere specifications with what you want to deal with.
This example is basic one from universal algebra, which are theories you can cast positively in terms of positive constants (symbols) that don't even need existential quantifiers.
https://en.wikipedia.org/wiki/Universal_algebra 
