On Jun 13, 7:51 pm, Nam Nguyen <namducngu...@shaw.ca> wrote: > mikekell...@googlemail.com wrote: > > On Jun 10, 4:42 am, Nam Nguyen <namducngu...@shaw.ca> wrote: > >> MoeBlee wrote: > >>> Checking for correct > >>> application is a mere matter of applying a recursive procedure in > >>> pattern matching. > >> Right. As long as what contains the patterns is valid in the first place. > > > And how do we know what "patterns" are valid? > > > My answer would be something like: we specify the formal language, the > > axioms, and the rules of inference. Then we know a wff is one that is > > in the language. > > And a theorem is anything obtained from an axiom or > > another theorem by a rule of inference. > > > What's your answer? > > I've answered the "language" part of your answer many times in one way > or another, but let me answer again. A formula is is a string of symbols > written left to right in certain fixed patterns that we're supposed to know. > Based on those fixed patterns and on certain syntactical conventions, you > could discern whether or not a string follows the patterns. If it doesn't > you know it isn't a wff. If it does, you could discern how many non-logical > symbols there are and what kind each non-logical symbol is. > > On the "theorem" part of your answer, my answer is this: "a theorem is > anything" _validly_ "obtained from an axiom or another theorem by rule[s] of > inference". Obviously from my point of view, your answer doesn't emphasize > on the word "_validly_". And that makes a huge difference in this debate. > > What I've been saying all along is basically this: > > - From the _syntactical_ study of FOL, "simply specifying a language" is > simply not good enough for your side to conclude Axy[x+y=0] from the > lone-axiom theory T = {x=y}, because language must be specified by > its use in formulas and a theorem must be the conclusion of the specified > formulas known as axioms, when _validly_ applying the rules. So, when > the language is not specified through axioms, there' no valid reason > to conclude a formula having vacuous symbols relative to the axiom[s] > is a valid theorem!
(1) A formal language can be defined unambiguously by a set of symbols and a grammar defining what combinations of the symbols are wffs. (2) This is independent of any deductive apparatus of formal systems. (3) There is a formal language (call it A) with the usual symbols and grammar of FOL and additionally in which + is a binary function and 0 is a constant. (4) There is a formal system which has A as its language and the usual logical axioms and inference rules of FOL, and the single non-logical axiom AxAy x=y. (5) In this formal system, x+y=0 is a theorem.
It's not clear where your objections lie. I'd say the biggest sticking point is (4). However you also seem to have issues with (1), (2), (3), and (5).
You apparently believe that it is _impossible_ for a formal system with A as its language to have the axiom AxAy x=y. You are incorrect.
The formal language of a formal system does not depend on its non- logical axioms. The non-logical axioms of a formal system must be wffs in its language. This is the only restriction. They do not have to contain every non-logical symbol which is in the language of the formal system.
