Timeline for May we axiomatize by means of Gödel codes?
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 17, 2021 at 18:25 | comment | added | მამუკა ჯიბლაძე | Oh now I understand, thank you | |
| Jun 17, 2021 at 16:15 | comment | added | Andrej Bauer | @მამუკაჯიბლაძე: replace all outer $\forall$ with something like $\mathrm{UniversalClosure}$. The OP is just defining what it means to have a universal closure of a formula, i.e., $\mathrm{UniversalClosure}(\epsilon) = \epsilon$ if $\epsilon$ is closed, and $\mathrm{UniversalClosure}(\epsilon) = \mathrm{UniversalClosure}(\forall x_i \, \epsilon)$ if the first free variable in $\epsilon$ is $\epsilon_i$. The OP however likes to save on parentheses and writes $\mathrm{UniversalClosure}$ as $\forall$, to make things more intuitive. | |
| Jun 17, 2021 at 16:08 | comment | added | Frode Alfson Bjørdal | @მამუკაჯიბლაძე For example, $\forall\forall x_3\exists y(y>x_3\cdot x_4\cdot x_2)$ is $\forall x_4\forall x_2\forall x_3\exists y(y>x_3\cdot x_4\cdot x_2)$. | |
| Jun 17, 2021 at 16:02 | comment | added | მამუკა ჯიბლაძე | I see, thanks. Though I still don't understand the meaning of the double $\forall$, also in the second paragraph. | |
| Jun 17, 2021 at 15:56 | comment | added | Frode Alfson Bjørdal | @მამუკაჯიბლაძე Correction: $[\eta(\dot{x_i})]$ is short for $[\eta](\dot{x_i}/[x_i])$, where $\dot{~}$ is the function which takes a number to its numeral. | |
| Jun 17, 2021 at 15:40 | comment | added | Frode Alfson Bjørdal | As we may see, $\mathbf{R}$ should have the axiom $\vdash\forall(\delta\to\epsilon)\to(\forall\delta\to\forall\epsilon)$. | |
| Jun 17, 2021 at 15:29 | comment | added | Frode Alfson Bjørdal | @AndrejBauer As seen by my previous paragraph, lonely universal quantifiers secure universal generalisations of the axioms. I have in mind Hilbert style systems here. | |
| Jun 17, 2021 at 15:25 | comment | added | Frode Alfson Bjørdal | @AndrejBauer Lonely universal quantifiers are metalogical devices, bound by paragraph 2 of the question. So, e.g., $\forall(x_1 =x_0\to(x_0 =x_1\to x_0=x_1))$ is $\forall x_1\forall x_0(x_1 =x_0\to(x_0 =x_1\to x_1=x_0))$. | |
| Jun 17, 2021 at 15:18 | comment | added | Frode Alfson Bjørdal | @AndrejBauer One may avoid generalization as a primitive inference rule if one axiom states that $\forall x\delta$ is an axiom if $\delta$ is an axiom, and one has $\forall x(\delta\to\epsilon)\to(\forall x\delta\to\forall x\epsilon)$ (Tarski? Cfr. e.g. G. Hunter, Metalogic, Part Three.) | |
| Jun 17, 2021 at 15:09 | comment | added | Frode Alfson Bjørdal | @მამუკაჯიბლაძე The double $\forall$s are defined in paragraph 2. In $\forall x_i\tau[\eta(\dot{x_i})]$, $\eta$ is a formula, and $\eta(\dot{x_i})$ is the formula resulting from substituting the occurrences of $x_i$ in $\eta$ with the numeral $\dot{x_i}$ denoting $[x_i]$. So $\eta(\dot{x_i})$ is $\eta(\dot{x_i}/[x_i])$. | |
| Jun 17, 2021 at 14:49 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
] to )
|
| Jun 17, 2021 at 6:27 | comment | added | Andrej Bauer | Can you be a bit more explicit about "only modus ponens as inference rule". Your logic has the universal quantifier, how are you ever going to prove anything involving $\forall$, or use it, if there are no rules for $\forall$? In a similar fashion: modus ponens lets you eliminate an implication, but how do you intend to prove an implication (you don't have any rules for that). Are we talking natural deduction or Hilbert system here? | |
| Jun 17, 2021 at 3:46 | comment | added | მამუკა ჯიბლაძე | Maybe this is standard notation but what are these double $\forall$s, and what is $\eta(\dot{x_i}]$? | |
| Jun 17, 2021 at 3:21 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
Last line corrected with $\forall$
|
| Jun 17, 2021 at 2:47 | history | edited | Frode Alfson Bjørdal | CC BY-SA 4.0 |
Corrected an error in $A^{\tau 4}$
|
| Jun 17, 2021 at 2:40 | history | asked | Frode Alfson Bjørdal | CC BY-SA 4.0 |