Search Results
Search type | Search syntax |
---|---|
Tags | [tag] |
Exact | "words here" |
Author |
user:1234 user:me (yours) |
Score |
score:3 (3+) score:0 (none) |
Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
Views | views:250 |
Code | code:"if (foo != bar)" |
Sections |
title:apples body:"apples oranges" |
URL | url:"*.example.com" |
Saves | in:saves |
Status |
closed:yes duplicate:no migrated:no wiki:no |
Types |
is:question is:answer |
Exclude |
-[tag] -apples |
For more details on advanced search visit our help page |
first-order and higher-order logic, model theory, set theory, proof theory, computability theory, formal languages, definability, interplay of syntax and semantics, constructive logic, intuitionism, philosophical logic, modal logic, completeness, Gödel incompleteness, decidability, undecidability, theories of truth, truth revision, consistency.
0
votes
1
answer
155
views
How to ensure a clean conservative extension in general?
Suppose we have a logic $L$ and we have conservative extension $L'$. So, every theorem of $L'$ that can be expressed in $L$ is also a theorem of $L$.
This does not guarantee that $L'$ is "clean". In …
1
vote
Accepted
Can invariant of transitive reflexive closure in FOL+PA always been proven?
The answer can be found here:
http://www.staff.science.uu.nl/~ooste110/syllabi/peanomoeder.pdf
Most important part, theorem 1.9 ii.
With this theorem you can have some kind of sequence for which yo …
2
votes
3
answers
651
views
logics restricted in arithmetic hierarchy
Hello, I would like to know if this already has been researched.
There has been lot of research done, where logics are limited. They are often limited in the axioms or inference rules, which makes th …
1
vote
How to prove Con(PA) in ZFC?
You can also prove the consistency of PA with second order logic.
The key thing is that you need a higher order induction hypothesis. In first order logic + PA, the induction hypothesis are limited t …
1
vote
2
answers
1k
views
Is there a natural example of a second order proof that does not reduce to a first order pro...
Dear all,
This is a retry of question Would Wiles proof of Fermat theorem reduce if you fill in the variables?. I stated that question badly, but my intention are genuine and hope do to a better job …
1
vote
2
answers
429
views
Are Separation and Types the only way to avoid paradoxes?
When Russell discovered his paradox, two ways were invented to avoid Russell's paradox.
For logic with sets, ZFC was developed which restricts the creation of the definition of sets. Only sets that a …
1
vote
1
answer
513
views
Can invariant of transitive reflexive closure in FOL+PA always been proven?
I am trying to understand FOL + PA, better.
With FOL + PA I mean, first order logic, with addition and multiplication predicate and induction axiom scheme.
The book I am reading explains how to cons …
5
votes
3
answers
2k
views
Can the omega-rule rescue Hilbert's program?
As known the second incompleteness theorem derailed Hilbert's program.
However, Hilbert himself tried to rescue it with the $\omega \text{-rule}$, according to the following paper:
http://repository …
9
votes
1
answer
633
views
Starting Hilbert's Program on the other end
The idea of Hilbert's program was to start with a simple finitary logic and proof the consistency of more complex systems in this system. Of course, this turned out to be problematic. Even when absolu …
3
votes
1
answer
146
views
Defining functions in FOL + PA
I am looking into the practicalities of doing Math in FOL + PA with the FOL extended with equality and functions.
For a predicate you can easily extend the language such that a predicate is defined as …
5
votes
2
answers
341
views
Can a universal induction rule be formulated?
$\newcommand{\Con}{\operatorname{Con}}$The intention of Hilbert's program was to start with a simple logic and then justify more complex logics from there. So, we get a sequence of logics:
$$
L_1 → L_ …
5
votes
2
answers
933
views
Program transformation as alternative for Hoare logic or temporal logic
After such transformation, formal (that is why I tagged with lo.logic) reasoning can be done about the program. …
1
vote
0
answers
510
views
Single logic foundation vs. multi-logic foundation
Dear all,
I have always wondered why I have never read anything about this topic. My question is, are there are any books or articles covering this subject?
With this topic I mean the philosophical …
5
votes
1
answer
628
views
What are key $\Sigma^0_2$ or $\Pi^0_3$ theorems?
I am researching a logical system that is limited to $\Pi^0_2$ sentences and I am busy to prove that FOL + PA is a conservative extension of that system. Meaning that with $\Sigma^0_n$ sentences (that …
4
votes
2
answers
278
views
Is there any literature about inner-replacement rule?
Hello all,
If you have a theorem $\vdash \alpha \rightarrow \beta$ and a theorem $\vdash \gamma$ then if $\alpha$ is a sub-expression of $\gamma$, and this sub-expression has an even number of negati …