# Questions tagged [formal-systems]

A formal system is broadly defined as any well-defined system of abstract thought based on the model of mathematics. (Def: http://en.m.wikipedia.org/wiki/Formal_system)

258 questions
Filter by
Sorted by
Tagged with
0 votes
0 answers
26 views

### Is there a Turing degree/number of unknowns combination beyond which Diophantine equations are independent of PA?

Is there a certain limit in terms of Turing degree and # of unknowns beyond which Diophantine equations (for positive integer solutions) are independent of PA? Specifically, is it meaningful to talk ...
1 vote
0 answers
35 views

### Is Kleene's realizability recursive?

Kleene introduced realizability as a practical semantical interpretation of Heyting Arithmetic (see link for definition). The key result he proved is that provability of $\varphi$ in HA implies the ...
• 11
1 vote
0 answers
46 views

### Why can't we add a self-consistency axiom to an already consistent system?

Gödel's incompleteness tells us no consistent formal system can prove its own consistency. I understand that we can add an axiom to formal system $A$ stating "$A$ is consistent" and get a ...
1 vote
0 answers
52 views

### Is it coherent to treat the C programming language as a formal system?

In mathematical logic, a formal system is a structure which includes, amongst other things, a set of axioms, and which is able to determine the truth or falsehood of statements with respect to those ...
• 145
0 votes
1 answer
32 views

### Definition of Locus in Synthetic Geometry?

How is "locus" defined in Euclidean geometry? I know that locus is defined as a set of all points satisfying a certain condition. But how do we define "locus" within an axiomatic ...
2 votes
1 answer
35 views

### How does the finitely axiomatized formalization of predicate logic correspond to natural deduction for predicate logic?

I'm really interested in using Metamath, but Metamath comes with a funky version of predicate logic. Substitution is not allowed in Metamath, so Metamath employs Tarski's system S2 which is "...
0 votes
0 answers
56 views

• 65.1k
0 votes
0 answers
33 views

### What differences and relation are between proof systems and deductive systems? [duplicate]

https://en.wikipedia.org/wiki/Proof_calculus says A proof system includes the components: Language: The set of formulas admitted by the system, for example, propositional logic or first-order logic. ...
• 43.6k
8 votes
2 answers
283 views

### What's up with the Sheffer stroke axiom?

While reading some old paper on the foundations of set theory, I came across a symbol $\mid$ that I eventually determined was the Sheffer stroke, which is a fancy word for NAND. Wikipedia, and also ...
• 113k
5 votes
2 answers
349 views

### Implementing sets in $\lambda$-calculus

Both Set theory and $\lambda$-calculus are considered to be valid foundations for mathematics. Since these are both equivalent (in the sense that any structure that can be implemented in set theory ...
• 510
1 vote
1 answer
95 views

### Why doesn't this show that first-order Peano arithmetic is consistent?

SOME PRELIMINARIES: Predicate logic is consistent and complete. In other words, (i) for a closed formula $F$ in predicate calculus with equality and functions, $\vdash F$ if and only if $\,\vDash F$ (...
• 1,009
21 votes
2 answers
2k views

### What is the definition of a definition?

In mathematical logic or other formal systems, what is the definition of a definition, formally? If "A" is defined as "B", what is the definition of "A" like? Does it ...
• 43.6k
4 votes
1 answer
378 views

### Can inconsistent systems be mathematically interesting/useful?

According to the top answer to this question: Doing mathematics we often have an idea of an object that we wish to represent formally, this is a notion. We then write axioms to describe this notion ...
0 votes
1 answer
274 views

• 24.8k