Timeline for Can Basic Law $V$ be derived from Leibniz's Law in Second-Order Logic without comprehension principles?
Current License: CC BY-SA 3.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 14, 2016 at 12:02 | comment | added | Thomas Benjamin | (cont.) but I want to check. If I have not made a mistake in logic here, I will gladly post my comments as an answer. | |
| Jun 14, 2016 at 11:57 | comment | added | Thomas Benjamin | @JacquesCarette: Sorry to keep you on 'hold' so long, but I was waiting for Mauro Allegranza to answer my comment before yours. If '$x$' satisfies both '$F$($x$)' and '$G$($x$)', and since $x$=$x$ $\land$ $x$=$x$$\equiv$ $x$=$x$, is it correct to infer from ($\forall$$F$)($F$$x$$\equiv$$F$$x$)$\equiv$$x$=$x$ $\land$ ($\forall$$G$)($G$$x$$\equiv$$G$$x$)$\equiv$$x$=$x$, ($\forall$$F$)($F$$x$$\equiv$$F$$x$)$\equiv$($\forall$G$)($$G$$x$$\equiv$$G$$x$)$\equiv$$x$=$x$, and from this correctly infer ($\forall$$F$)($\forall$$G$)($F$$x$$\equiv$$G$$x$)$\equiv$$x$=$x$? I believe it is, | |
| Jun 9, 2016 at 23:20 | comment | added | Jacques Carette | Might it not be nice to turn some of this into an answer? Reading a whole lot of comments is not nearly as pleasant. And *Overflow has this way of attracting Google hits, so for posterity, could someone wrap this up? | |
| Jun 9, 2016 at 9:08 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: I assume '$x$' satisfies both '$F$($x$)' and '$G$($x$)' so one can form ($\forall$$F$)($F$$x$$\equiv$$F$$x$)$\equiv$ $x$=$x$ $\equiv$ ($\forall$$G$)($G$$x$$\equiv$$G$$x$). I take it that this formula is invalid in general (obviously it is, since your example is correct). What then is the correct way to write what I am trying to say, then? | |
| Jun 9, 2016 at 8:44 | comment | added | Mauro ALLEGRANZA | From the fact that $(∀F)(Fx≡Fx)$ and $(∀G)(Gx≡Gx)$ - that are obviously true - you cannot derive: $(∀F)(∀G)(Fx≡Gx)≡ x=x$: the RHS is valid, while the LHS: $(∀F)(∀G)(Fx≡Gx)$ says that every object has all the properties... Think at $Odd(x) ≡ Even(x)$ | |
| Jun 8, 2016 at 22:12 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: The rest should follow easily (except for possibly the substitutions of ' $\hat x$$F$$x$', $\hat x$$G$$x$ for either side of $z$=$z$....). | |
| Jun 8, 2016 at 21:24 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: Correct. That was a typo. It should read, "from $x$=$y$$\equiv$($\forall$$F$)($F$$x$$\equiv$$F$$y$) one can derive $x$=$x$$\equiv$($\forall$$F$)($F$$x$$\equiv$$F$$x$) by substituting '$x$' for '$y$' " (that's the problem with the five minute edit rule for comments....) | |
| Jun 8, 2016 at 13:24 | comment | added | Mauro ALLEGRANZA | In your first comment above you go from $x =y≡ (∀F)(Fx≡Fy)$ to $x=x≡(∀x)(Fx≡Fx)$. This is not correct; you must have $x=x≡(∀F)(Fx≡Fx)$. You cannot subst for a function var an object var. | |
| Jun 7, 2016 at 12:04 | comment | added | Thomas Benjamin | (cont.) ($\forall$x)($F$$x$$\equiv$$G$$x$)$\equiv$ $\hat x$$F$$x$=$\hat x$$G$$x$--Basic Law $V$. I cannot claim that this is a 'proof'--only a philosophical argument-- but this philosophical argument might suggest why Frege thought that Basic Law $V$ was a 'law of logic'. | |
| Jun 7, 2016 at 11:59 | comment | added | Thomas Benjamin | (cont,) ($\forall$$F$)($\forall$$G$)($\forall$$x$)($F$$x$$\equiv$$G$$x$)$\equiv$ ($\forall$$z$)($z$=$z$). By Elimination of Quantifiers, one can eliminate '$\forall$$F$', '$\forall$$G$', and '$\forall$$z$' and derive ($\forall$$x$)($F$$x$$\equiv$$G$$x$)$\equiv$ $z$=$z$. Since '$x$' satisfies both '$F$' and '$G$', the terms '$\hat x$$F$$x$', '$\hat x$$G$$x$' refer to the same elements, one can seemingly (and here is where a problem may lie) substitute the term '$\hat x$$F$$x$' to one side of '$z$=$z$' and $\hat x$$G$$x$ to the other to derive | |
| Jun 7, 2016 at 11:26 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: I believe I have the requisite substitutions. From '$x$=$x$, since one can substitute '$z$' for '$x$' and '$x$' for '$z$, one can derive $x$=$x$$\equiv$$z$=$z$. Also, since $x$=$x$ and $z$=$z$ for all '$x$', '$z$', one has ($\forall$$x$)(x=x)$\equiv$($\forall$$z$)($z$=$z$). Similarly, since ($\forall$$F$)($\forall$$G$)($F$$x$$\equiv$$G$$x$)$\equiv$ $x$=$x$, one can infer ($\forall$$F$)($\forall$$G$)($\forall$$x$)($F$$x$$\equiv$$G$$x$)$\equiv$ ($\forall$$x$)($x$=$x$), one has (by transitivity of $\equiv$), | |
| Jun 7, 2016 at 8:14 | comment | added | Thomas Benjamin | (cont.) ($\forall$$F$)($\forall$$G$)($F$$x$$\equiv$$G$$x$) $\equiv$ $x$=$x$ (as one can see, this is getting 'close' to deriving Basic Law $V$). From here, the question now becomes: how to handle the appropriate substitutions and definitions of 'objects' in order to derive Basic Law $V$. Can one appropriately arrange 'substitions' and 'definitions of objects' in SOL in order to derive Basic Law $V$? | |
| Jun 7, 2016 at 7:54 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: Consider the following 'derivation': From $x$=$y$$\equiv$($\forall$$F$)($F$$x$$\equiv$$F$$y$) one can derive $x$=$x$$\equiv$($\forall$$x$)($F$$x$$\equiv$$F$$x$) by substituting '$x$' for '$y$'. Assuming '$x$' has another property ' $G$', one can also write $x$=$x$$\equiv$($\forall$$G$)($G$$x$$\equiv$$G$$x$). Since $x$=$x$ $\land$ $x$=$x$ $\equiv$ $x$=$x$, one can write (because $\equiv$ is symmetric) ($\forall$$F$)($\forall$$G$)($F$$x$$\equiv$$F$$\equiv$$G$$x$$\equiv$$G$$x$) $\equiv$ $x$=$x$. From this, one can derive | |
| Jun 4, 2016 at 10:01 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: It should be noted that in Manuel Bremer's preprint "Frege's Basic Law ($V$) and Cantor's Theorem", he writes Basic Law $V$ this way: ($\forall$$ F$)($\forall $$G$)($\hat e$$F$($e$)=$\hat e$$G$($e$)$\equiv$($\forall$$x$)($F$($x$)$\equiv$$G$($x$))). Is this not a correct way of writing Basic Law $V$? | |
| Jun 3, 2016 at 18:41 | comment | added | Mauro ALLEGRANZA | I think that you cannot derive BL V from L's law without extra assumptions: SOL (equality axioms included) is consistent, while Frege's system (with BL V) is not. | |
| Jun 3, 2016 at 17:29 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: I find it interesting that Zalta states that the rule of uniform substitution is logically equivalent to the Comprehension Principle for Concepts without referwnce to Basic Law $V$.... | |
| Jun 3, 2016 at 14:17 | comment | added | Mauro ALLEGRANZA | BL V and L's law are only apparently similar: the first one quantify on "objects", while the second quantify on "functions". And the issue with F's original system is exactly in the assumption that for every function there is a corresponding object (its wertverläufe). | |
| Jun 3, 2016 at 14:13 | comment | added | Mauro ALLEGRANZA | Leibniz's law is Basic Law III of Gg. | |
| Jun 3, 2016 at 14:12 | comment | added | Mauro ALLEGRANZA | You can see Frege's Rule of Substitution; in general, for Frege's logic, see Zalta's entry on Frege's Theorem. | |
| Jun 3, 2016 at 13:49 | comment | added | Thomas Benjamin | @MauroALLEGRANZA: Interesting. How so? Also, does Frege realize they are so "embedded"? | |
| Jun 3, 2016 at 13:25 | comment | added | Mauro ALLEGRANZA | In Frege's system there are "comprehension principles"; they are "embedded" into Grundgesetze's rule of uniform substitution. | |
| Jun 3, 2016 at 11:26 | history | edited | Thomas Benjamin | CC BY-SA 3.0 |
corrected spelling
|
| Jun 3, 2016 at 10:54 | history | asked | Thomas Benjamin | CC BY-SA 3.0 |