Skip to main content
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
Search options not deleted user 9896

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
5 answers
345 views

"local variables" in first-order formulas

Often in logic, you want to define a formula $\phi(x)$ which "says something about $x$". For example, $\phi(x)$ may say that $x$ is a prime. In order to form $\phi$, you may need internal bound variab …
David Harris's user avatar
  • 3,475
42 votes
4 answers
2k views

Inconsistent theory with long contradiction

What can one say about an inconsistent theory $T$ which has no contradictions (i.e. deductions of $P \wedge \neg P$) of length shorter than $n$, where $n$ is some huge number? There have been some di …
David Harris's user avatar
  • 3,475
0 votes

Seemingly complex logic/set-theoretic puzzle

Based on the answers proposed to this question, I think this problem is ill-defined. The set of possible questions and assignment of truth valuations is not well defined. A fair definition of a "quest …
David Harris's user avatar
  • 3,475
1 vote
Accepted

Equivalence of monadic axioms

The comment showed that decidability of axiom equivalence is implied by decidability of pure logic. (I.e. to decide if $\Theta$ and $\Theta'$ are equivalent, it is equivalent to decide if $\vdash \The …
David Harris's user avatar
  • 3,475
5 votes
2 answers
825 views

Semantic definition of sentence

This is a follow-up to question Completeness vs Compactness in logic 68788. One common theme was that compactness in logic is a purely semantic notion, so should have no need of completeness. The def …
David Harris's user avatar
  • 3,475
15 votes
1 answer
813 views

Undecidable theories easier than $Q$

Most proofs of undecidability for various theories (pure logic with binary relation, group theory, etc.) show that the natural numbers and Robinson's $Q$, in one form or another, can be encoded approp …
David Harris's user avatar
  • 3,475
1 vote
5 answers
2k views

Why do we ignore non-standard finite sets in ordinary mathematics?

Here is a how a typical proof might look like in group theory--- Suppose we are given a finite group $G$. Enumerate the elements $g_1, \dots, g_n$. Now consider a formula $\phi(g_1, \dots, g_n)$ which …
David Harris's user avatar
  • 3,475
16 votes
2 answers
3k views

Can randomness add computability?

I have been looking at Church's Thesis, which asserts that all intuitively computable functions are recursive. The definition of recursion does not allow for randomness, and some people have suggested …
David Harris's user avatar
  • 3,475
6 votes

Is P=NP relevant to finding proofs of everyday mathematical propositions?

The point is that, if P=NP, there would exist a universal algorithm (applicable not just to specific theorems) that would find proofs in time polynomial in length of the proof. Most important results …
David Harris's user avatar
  • 3,475
23 votes
10 answers
5k views

Completeness vs Compactness in logic

One standard approach to showing compactness of first-order logic is to show completeness, of which compactness is an easy corollary. I am told this approach is deprecated nowadays, as Compactness is …
David Harris's user avatar
  • 3,475
4 votes

How do they verify a verifier of formalized proofs?

One simple suggestion no-one seems to have mentioned is to have the verifier prove itself correct. Obviously, this cannot really give any assurance that the verifier is correct, since if the verifier …
David Harris's user avatar
  • 3,475
5 votes

Are there examples of nonconstructive metaproofs?

If the proof system is recursively axiomatizable, this situation cannot occur. If there exists a proof of $\Theta$, there exists an algorithm to find that proof. Namely, search the recursively enumer …
David Harris's user avatar
  • 3,475
4 votes
1 answer
725 views

Proof system with same complexity as "informal mathematics"?

The Completeness Theorem in first-order logic states that any mathematical validity is derivable from axioms. Hence, any informal mathematical proof (which is rigorous) can be translated into a formal …
David Harris's user avatar
  • 3,475
14 votes
3 answers
3k views

Definition of relativization of complexity class

Is there any general definition, for a class $C$ of languages, what is the relativized class $C^A$ for an oracle $A$? Usually, these classes and their relativizations seem to be defined in an ad-hoc …
David Harris's user avatar
  • 3,475
2 votes

Why is it OK to rely on the Fundamental Theorem of Arithmetic when using Gödel numbering?

Here is a way to think about it. When you use something like Fund Theorem of Arithmetic to prove Godel numbering, you are referring to the abstract set $\mathbf N$, which "exists". The Fundamental The …
David Harris's user avatar
  • 3,475

15 30 50 per page