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 3154

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.

7 votes

How much of the current logic is about syntax?

We don't know how to abstract away from syntax in proof theory. If we say there are three main branches in proof theory: Axiomatics seem to be necessarily syntactic: formulae are what it is about; …
Charles Stewart's user avatar
5 votes

What does it mean for a mathematical statement to be true?

Both the optimistic view that all true mathematical statements can be proven and its denial are respectable positions in the philosophy of mathematics, with the pessimistic view being more popular. T …
1 vote

Formulas for the liar paradox

Aladdin M. Yaqūb (1993) The Liar Speaks the Truth, OUP, formalises a very simple language for naturally expressing the liar paradox, consisting of: First-order equational logic which may, but need n …
Charles Stewart's user avatar
2 votes

cut elimination

To elaborate on Alexey's answer, for "usual" sequent calculi, the rules other than cut "build structure" in the proof: the left rules build up structure of the assumptions from smaller formulae, and t …
Charles Stewart's user avatar
4 votes

Where are we working when we prove metamathematical theorems?

Real Logicians(*) use primitive recursive arithmetic as their metatheory. As a purely equational, and so unquantified, theory, it is agnostic about the distinction between classical and intuitionisti …
Charles Stewart's user avatar
5 votes

What does it mean to 'discharge assumptions or premises'?

In the spirit of Kenny's observation, note also that we can formulate classical logic using a Peircian inference rule (equivalent to the usual theory in the presence of ex falso quodlibet) which clear …
Charles Stewart's user avatar
2 votes

Are all mathematical theorems necessarily true?

John Goodrick writes, very much to the point: The last I heard, there was no consensus in the philosophical community as to what exactly a "possible world" is, or whether this is even a coherent notio …
Charles Stewart's user avatar
10 votes
Accepted

What does the disjunction elimination rule say?

The first rule is not the regular disjunction elimination rule, but is known as disjunctive syllogism, and is essentially the modus tollendo ponens rule of term logic. The two rules are mutually admi …
Charles Stewart's user avatar
5 votes

When is something too big to be a set?

I find the terminology of "too big" to be misleading. I think it comes about from thinking that the strength of a set theory comes from the generosity of its comprehension axioms, that stronger set t …
Charles Stewart's user avatar
4 votes

Can we prove set theory is consistent?

I think you are describing a process that is a fairly accurate description of how set theorists typically think about issues of consistency, where Set1 is the informal account of the cumulative hierar …
Charles Stewart's user avatar
9 votes

Most general formulation of Gödel's incompleteness theorems

Theories can be be represented recursion-theoretically by an encoding of the language as natural numbers (most simply, a bijective encoding, which I assume), and a Turing machine that accepts all and …
Charles Stewart's user avatar
3 votes
Accepted

Can infinite first-order categories be specified other than as categories of models?

Sure, by direct construction. Rings, preorders, the category of paths of a given graph, etc. But that's not what you wanted to know, is it?
Charles Stewart's user avatar
8 votes

Do you know any good introductory resource on sequent calculus?

Gentzen, 1934, 'Investigations into Logical Deduction' — This is very readable, and introduces so many ideas that later synthetic works invariably miss some. If you're serious, this, and some other p …
Charles Stewart's user avatar
4 votes

How do they verify a verifier of formalized proofs?

The key point is the idea of the kernel of a theorem prover, as Adam mentioned. To put it another way the kernel is the smallest subset of the theorem prover's code base (and operating system and mac …
Charles Stewart's user avatar
7 votes
Accepted

Is there a relationship between model theory and category theory?

Between model theory and category theory broadly conceived: not anything really compelling, because a category, on its own, does not stand as an interpretation for anything. Between model theory and …
Charles Stewart's user avatar

15 30 50 per page