Talk:Free logic

Is 1b really a substitution instance of 1? I suspect the author wanted to say that 1b is a substitution instance of 1a (and, in the next paragraph, that 1a (instead of 1) implies from "everything identical with Pegasus is Pegasus" to "something is identical to Pegasus"). But then the question becomes: is 1b really a substitution instance of 1?

I have modified the formulas accordingly. The formula A was not meant to be atomic where Ax is a monadic predicate. Nortexoid 02:02, 13 July 2005 (UTC)

Unicorns

You can only infer that "there is a unicorn" using your (1) if you have the hypothesis "everything is a unicorn". [this is changed from the original to address the following objection] This is really not a serious problem as the hypothesis seems very unlikely. A better example is the observation that the axiom of the empty set, for which many of us feel a need in Zermelo set theory (or ZFC), is redundant, because logic tells us that there is a set (since the class of sets is the domain of the quantifiers in ZFC) and then Separation gives us the empty set from any set. Randall Holmes 06:34, 5 January 2006 (UTC)

That is not true, since we can infer existential generalizations from unquantified sentences by the valid inference schema $P(a_{1},...,a_{n})\supset \exists x_{1},\dots ,\exists x_{n}P(x_{1},...,x_{n})$. Nortexoid 01:38, 6 January 2006 (UTC)

Let U be the predicate "there is a unicorn": it is indeed valid that $U(a)\rightarrow (\exists x.U(x))$, but one cannot deduce $(\exists x.U(x))$ from this without the additional premise $U(a)$ (you cannot show that there is a unicorn without postulating a specific unicorn, even in classical, non-free, formulations of FOL).

You're right--it will be removed. Nortexoid 02:39, 6 January 2006 (UTC)

The point of my remarks is that the assertion

• From (1) in the unrestricted predicate calculus, if A is 'is a unicorn' it can be inferred that a unicorn exists.

in the article is wrong. Please change it.

There are other serious problems with what you say here. For example, in standard FOL, there simply can't be a term denoting Pegasus, so you cannot make the substitution you describe. I am reluctant to edit the article myself, because if I do I shall simply rewrite it from first principles.

 Randall Holmes 01:57, 6 January 2006 (UTC)

That is true but nowhere in the article have I said that the substitution is permissible in classical FOL. In any case, feel free to rewrite the article if you wish. Nortexoid 02:39, 6 January 2006 (UTC)

Rewrites

I have rewritten the text so that it doesn't contain any obvious errors. Your 1a was not a substitution instance of (1) in any obvious sense, so I relabelled it as (4); in (1a) and related sentences the scopes of the quantifiers were not what I would expect, so I adjusted them. The scheme $(\forall x.Fx\rightarrow Gx)\rightarrow (\exists x.Fx\wedge Gx)$ is not valid, so I omitted it. The existence predicate is usually a primitive in free logic; the definition you give may actually always be valid, but I need to check that (there are at least two essentially different systems of free logic). Randall Holmes 14:56, 6 January 2006 (UTC)

There are a lot of errors in this article! $\forall xA\rightarrow \exists xA$ isn't a theorem of classical logic. --Dante

There are a lot of errors in your head! That is a theorem of classical logic. Please don't edit the article. Nortexoid 20:26, 26 November 2006 (UTC)

I agree. However I don't agree that it's not valid in the empty universe. Granted it is not true in the empty universe, but validity is not truth or no one would make that distinction. A sentence is valid when it is true for every assignment of values to the variables of the language. But if there are no values there can be no assignments, so even though the sentence cannot be true it is nevertheless vacuously valid. This whole article is predicated on fallacious reasoning that was accepted by all logicians prior to around 1980 when the fallacy was first noticed. --Vaughan Pratt (talk) 03:23, 29 May 2010 (UTC)

A formula is valid iff it is true on every model for the language and it is true on a model just in case it is satisfied in that model for every assignment defined relative to that model (where satisfaction is defined recursively as usual). Since, in this setting, models are classical except with partial, rather than total, assignments, the implication mentioned above is equivalent to Ex~A(x) v ExA(x). A disjunction is true iff at least one of the disjuncts is true, and one of those existential formulae is true iff there is an assignment taking 'x' to some element of the domain which satisfies A(x). According to these standard definitions such a formula won't be satisfied in the empty model and hence won't be true in the empty model and hence it won't be valid since it's not true one every model. There's no fallacious reasoning involved here unless you wish to take objection to the adequacy of the definitions of 'true on a model', 'satisfied in a model relative to an assignment', or 'valid'. Nortexoid (talk) 10:01, 29 May 2010 (UTC)

What is 2 & 3 doing! 1. "not free" contains the possibility of not defined. 2. I then tried to change the statement many times, but I can't find a good enough way to avoid contradiction. I will change it to a much weaker description. — Preceding unsigned comment added by The193thdoctor (talk • contribs) 01:17, 16 September 2019 (UTC)

Logical consequence or material conditional?

I added a corresponding clarification request with more detail, but basically some of the equations in this arrow use a $\Rightarrow$ while others use a $\rightarrow$, and so I'm not certain whether both arrows are meant to denote/connote the same thing, and whether that same thing is material conditional or logical consequence (i.e. semantic consequence). 69.143.122.185 (talk) 16:25, 28 January 2023 (UTC)