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 | |
Results tagged with lo.logic
Search options not deleted
user 3118
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.
1
vote
Impredicativity
Type Theory is worthwile alone for its practical applications. So if you dont like it as a foundation of mathematics, accept it as applied mathematics.
On the other hand, predicative definitions are …
0
votes
Is there a natural example of a second order proof that does not reduce to a first order pro...
Firstly, when using natural deduction rather than a sequent calculus, it is fairly straightforward to algorithmically replace an induction step for a given $n$ by the actual proof for this special $n$ …
5
votes
When are two proofs of the same theorem really different proofs
You can express any Proof as a typed Lambda-Term, looking at the theorem as a Type. This term can be normalized. I would say, if two of these Proof-Terms have the same normal form, then they name the …
0
votes
Naturally definable sets of natural numbers
In general, I consider this question interesting. But on the other hand - well, you don't specify what literals you accept in your formal System.
If you have $\le$ for example, it is likely that you …
0
votes
Does the axiom of specification prevent writing any proof?
I think with such problems it helps to make it clear what the syntactical rules actually "mean". The rule you mention sais that - basically - if you dont have any further assumptions about a term $t$ …
0
votes
Which classes are sets?
It may not completely fit, but - just to have said that - in Zermelo-Fraenkel Set Theory, there are no classes. Classes are a concept of the meta-theory - a "class" is no object inside any model of ZF …
2
votes
1
answer
511
views
What follows from assuming not Con(ZF)?
Hello.
Let $\operatorname{sat} X$ denote the satisfiability of a theory $X$.
From Gödel's second incompleteness theorem and his completeness theorem follows $$ZF \not\vdash \lceil \operatorname{sat} …
2
votes
What is the general opinion on the Generalized Continuum Hypothesis?
I am Formalist. And from a formal point of view, GCH is independent from ZF(C) - nothing more. To me, sets are not really "existing" (have you ever seen an infinite ordinal flying around somewhere? we …
0
votes
Can transfinite induction be defined as axiom scheme in FOL on bin-tree structures?
Not sure whether I understand what exactly you mean. But transfinite induction is formally almost the same as "finite" induction, the only difference lies in the limit-ordinal-case. I.e. "finite" indu …
3
votes
0
answers
240
views
Non-Computational classical subterms
Assume we have a proof term of the form $(a^{A\rightarrow^c B\rightarrow^{nc} C}b^Ac^B)^C$, where $c$ is classical (that is, contains free instances of duplex negatio affirmat). The extracted term wou …
8
votes
1
answer
2k
views
What fails when using call/cc as realizer of the Peirce formula
Define the axiom constants $p_{A,B}^{((A\rightarrow B)\rightarrow A)\rightarrow A}$ as realizers of the Peirce formula, and $f_A^{\bot\rightarrow A}$ as realizers of the Ex Falso Quodlibet. Then $p_{A …
5
votes
Why can't proofs have infinitely many steps?
Somewhat semi-related, but I think also fitting here since connected to infinitary logic, are oracle-turing-machines. In the end, an Oracle can solve the finite Entscheidungsproblem - for your countab …
2
votes
Theory mainly concerned with $\lambda$-calculus?
Untyped Lambda Calculus is part of the Recursion Theory, I would say. Typed Lambda Calculus is Type Theory, and is connected with constructive mathematics.
The Lambda-Calculus is a concept that can b …
17
votes
Function extensionality: does it make a difference? why would one keep it out of the axioms?
You will lose canonicity, which is - mathematically - not that much of a problem, but when you want to extract programs, you want it. The problem is that not every proof of equality reduces to reflexi …
10
votes
5
answers
5k
views
Examples of inductive proofs that can be generalized by transfinite induction
Hello. I am currently searching for some nice examples of proofs by induction in the finite case, that can be generalized to the infinite case using transfinite induction (and dont become trivial ther …