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)

Filter by
Sorted by
Tagged with
-2 votes
1 answer
206 views

Why Löwenheim–Skolem theorem asserts the non-existence of such predicates in 1st order logic

Suppose there was a predicate, in the language of 1st order $ \mathsf {PA} $, such that it is only true for standard natural numbers i.e. it accepts ALL and ONLY standard natural number, and it ...
Alex Matyasaur's user avatar
0 votes
1 answer
42 views

Meaning of Provable recursiveness

Is there any difference between provably total function and provable recursiveness of a function in first order PA ? From provably total I mean that the totality of the function itself is provable in ...
user avatar
1 vote
0 answers
104 views

How to prove the property of being a tautology is hereditary under the Rule of Substitution?

In Appendix of Godel' proof by Nagel, there is a proof being left to the reader. The proof is how to prove the property of being a tautology is hereditary under the Rule of Substitution? I have no ...
cylia's user avatar
  • 11
0 votes
2 answers
127 views

Circularity in the argument that Gödel's incompleteness theorems undermine Hilbert's program

I'm only familiar with the very basics of mathematical logic, but over the last few days I have been looking into Gödel's incompleteness theorems and it seems to me (but I might simply be grossly ...
Inzinity's user avatar
  • 1,713
1 vote
0 answers
97 views

Can Bayesian analysis address challenges posed by Gödel's incompleteness theorems?

In short, according to Gödel's incompleteness theorems, if a formal mathematical system is consistent, then it will contain true statements that can neither be proven nor disproven it will be unable ...
RyRy the Fly Guy's user avatar
1 vote
0 answers
64 views

Connection of axioms of first order logic and axioms of first order theory

If we have a set of sentences S in first order logic. We know that we can create a first order theory Th(S) from S, which is the "set S" union "the sentences which we can prove them ...
zaxsqwedc's user avatar
0 votes
0 answers
54 views

Axiomatic system that differentiates between straight lines and curved lines

I was thinking about a formal system that involves a set of primitives along with a property that, when applied to the model of planar one-dimensional objects, can distinguish between straight lines ...
Soham Saha's user avatar
7 votes
1 answer
205 views

((())()) is a theorem of PR?

If we have the following formal system, called PR whose formulas are strings of well-formed parentheses. The language has two symbols '(' and ')'. Any expression is a formula. The only axiom is (). ...
Brian Andres's user avatar
0 votes
1 answer
72 views

Is there a consistent theory with self-similar set of theorems/axioms?

Does there exist a consistent theory (formal system) which has, say a set of axioms $\{A_1,A_2,\dots, A_n\}$ + rules of inference such that there is a proper subset of (non-trivial) theorems $\{T_1,...
Sergey Dylda's user avatar
5 votes
1 answer
182 views

Is there a proposition that cannot be proven to be provable(or not)? [duplicate]

I have been studying mathematical logic and the foundations of formal systems, and I came across the concept of "provability" and "unprovability" of propositions within such ...
suhdonghwi's user avatar
2 votes
1 answer
27 views

$(\lambda z. zy)(\lambda z. zy)$ - reducing using $\beta$ reduction and $\alpha$ conversion

Good day . I need to reduce the following expression of lambda calculus: $(\lambda z. zy)(\lambda z. zy)$ Now, since I am having the variable $y$ in both the left and right pair of parentheses, I ...
john doe's user avatar
  • 893
0 votes
0 answers
89 views

Reducing any formal system to intuitionistic or classical logic

Does the following provability hold in intuitionistic logic? $\vdash a_0\Rightarrow(a_1\Rightarrow(\dots\Rightarrow(a_n\Rightarrow a_k)\dots))$ for $0\leq k\leq n$ $a_0\Rightarrow (a_1\Rightarrow(\...
porton's user avatar
  • 5,029
6 votes
1 answer
239 views

Gödel on the “True Reason” for Incompleteness

In footnote 48a of his famous paper on incompleteness, Gödel writes: [T]he true reason for the incompleteness inherent in all formal systems of mathematics is that the formation of ever higher types ...
neddo's user avatar
  • 113
5 votes
0 answers
147 views

Do Tarski's axioms apply to higher dimensions?

I came across the wonderful fact that the theory of Euclidean geometry in 2 dimensions is complete, consistent and decidable — as shown by Tarski's axiomatization. I know very little about this. My ...
Alex's user avatar
  • 355
3 votes
0 answers
96 views

Can ZFC be proven from weak systems using consistency of those systems?

Tl;dr Can we take a weak system $A_0$ then show $$A_0 + Con(A_0)\implies Con(A_1)), \space A_1 + Con(A_1)\implies Con(A_2)), \space A_2 + Con(A_2) \implies \dots$$ terminating in ZFC? My understanding ...
Zoe Allen's user avatar
  • 4,237
0 votes
0 answers
46 views

Which language will be generated by the following grammar?

So i have $$ G = (V,\sum, S, P) $$ while $$ V = {S, A, B} $$ $$ \sum = {a,b,c}$$ and for P: $$ P:= \begin{cases} S \rightarrow & cA\ | \ bB, \\ A \rightarrow & c, \\ B \...
JohnGam's user avatar
  • 331
4 votes
3 answers
310 views

Axiomatic proof of $⊢(a→b)→(¬b→¬a)$ without using the deduction theorem

I'm trying to prove : $⊢(a→b)→(¬b→¬a)$ , or the contrapositive as a wff, using the following 6 axioms, the Hypothetical Syllogism rule, and Modus Ponens. ...
H.S's user avatar
  • 41
0 votes
1 answer
95 views

Prove $\vdash((\alpha\rightarrow\beta)\rightarrow\gamma)\rightarrow(\neg \gamma\rightarrow\alpha)$ in P.

Prove $\vdash((\alpha\rightarrow\beta)\rightarrow\gamma)\rightarrow(\neg \gamma\rightarrow\alpha)$ in $P$. In propositional calculus formal system $P$, three axioms could be used: (A1) $(\alpha\...
Galaxy's user avatar
  • 163
3 votes
1 answer
174 views

Clarification about positive definition of prime numbers in book Douglas Hofstadter "Gödel, Escher, Bach: An eternal golden braid"

I'm reading this book in Dutch. There is a part that keeps me puzzled. Maybe I don't fully understand (needing explanation) or suspect potential errors in the translation (needing verification). Could ...
tvo's user avatar
  • 193
3 votes
3 answers
188 views

Why does natural deduction get its name?

For example, I want to prove $\psi$ from the assumption $\{\varphi,\varphi\to\psi\}$ , the "most natural" proof would be: $\varphi$ $\varphi\to\psi$ $\psi$(MP) But using natural deduction, I ...
William's user avatar
  • 205
0 votes
1 answer
103 views

Are ZFC and Formal Number theory already built upon the intuitive notion of set and natural number? [duplicate]

These two theories are known to be first-order theories. And the definition of the first-order logic typically involves something like "set of symbols $a_1, a_2, a_3...$", which already ...
Sgg8's user avatar
  • 1,350
5 votes
0 answers
183 views

Reference for basic metatheory of Martin-Löf type theory

Section A.4 of the HoTT book states that the metatheoretic properties of Martin-Löf type theory (such as normalization and canonicity properties) can be proved using “standard techniques from type ...
simple jack's user avatar
0 votes
1 answer
142 views

What makes a set theory?

So many things get called "set theory" that I'm no longer sure the term is meaningful. This isn't helped by the rather vague notion of "formalizable in ZFC" used to avoid detailed ...
R. Burton's user avatar
  • 4,922
3 votes
1 answer
280 views

What does it really mean for a formal system to be consistent?

As far as I understand, asserting that a formal system $T$ is consistent means that there does not exist a sentence $\varphi$, expressed in the language of $T$, such that $T$ proves $\varphi$ and $T$ ...
Joe's user avatar
  • 19.5k
2 votes
0 answers
74 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 ...
Jori's user avatar
  • 101
1 vote
0 answers
81 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 ...
AsksQuestions's user avatar
1 vote
0 answers
67 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 ...
Tom Hosker's user avatar
1 vote
1 answer
46 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 ...
Steve Morris's user avatar
3 votes
1 answer
110 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 "...
Andrew Lubrino's user avatar
0 votes
0 answers
60 views

Given a formal system, determines if 4+3 = 7 is consistent

Given the formal system below: Language:$$\left\{ *,\blacksquare ,\blacklozenge \right\}$$ Syntax: $$ <s>::=<star>,"\blacksquare ",<star>,"\blacklozenge ",\ <star> $$ $$ <...
Avv's user avatar
  • 1,149
0 votes
1 answer
88 views

Representing first order sentences as conceptual graphs

Here are three first order axioms that represents a part of a mereology theory. Reflexivity $\forall x : part(x,x)$ Antisymmetry $\forall x \forall y : ((part(x,y) \land part(y,x)) \implies (x = y))$ ...
Patrick Browne's user avatar
0 votes
2 answers
87 views

Is the decidability of all possible axiomatizations equivalent to decidability?

Introduction This is a weird take on a few different topics in logic, so bear with me. To frame this question, consider that "axiomatization" is to "theory" as "...
R. Burton's user avatar
  • 4,922
0 votes
1 answer
56 views

How do we classify the obvious fact that $A \xrightarrow{gf} C$ can be decomposed into two arrows? Is it just notational?

The following image is of an app I'm working on called "Abstract Spacecraft". It will allow you to make logical rules and also apply them to diagrams at the click of a button, should the ...
Daniel Donnelly's user avatar
0 votes
2 answers
71 views

Generalization of nonexpressibility of solutions

Are there any ideas/areas of math that generalize the idea of when a solution to a question can be expressed in some given formal system? Something that (at least in spirit) covers results like No ...
nonagon's user avatar
  • 143
2 votes
0 answers
61 views

Help with metalogic induction proof involving string parsing

I have a formal language (basically language of first order logic) in which Wffs are defined by following. String $A$ is a Wff if it satisfies one of: $A$ is atomic $A \equiv (\lnot B)$ and $B$ is a ...
Jagerber48's user avatar
  • 1,298
0 votes
0 answers
87 views

Do we have to resort to intuition at the very root of our thinking?

Formal first order logic is the foundation of ZFC set theory. This gives me the impression that a theoretical system has to be based on a formal logical system, with its own axioms and deduction rules....
Ziqi Fan's user avatar
  • 1,816
0 votes
1 answer
170 views

Why isn't there an app that allows you to enter in all the rules of a given formal system so that the app supports all formal systems of math?

I'm jumping around between articles about ETCS to Simple TT to Calculus of Constructions wondering what my app should focus on. I'm wondering, why there isn't yet a software app in which you can ...
Daniel Donnelly's user avatar
0 votes
1 answer
196 views

Can you give an example of a non-formal system?

A formal system is defined as an abstract structure used for inferring theorems from axioms according to a set of rules (from Wikipedia). Language, logic and mathematics are considered as formal ...
highly oscillatory integrand's user avatar
5 votes
1 answer
151 views

Essential undecidability of binary string arithmetic

The weak theory of concatenation of binary strings is essentially undecidable.1 Is Presburger arithmetic with two successors (one for each letter) essentially undecidable? Formally, consider the ...
user76284's user avatar
  • 5,957
8 votes
0 answers
227 views

Precise statement of the syntactic category of a logic/type theory, in maximum generality?

I've been trying to understand the notion of syntactic category for a type theory/logic. This entry in the ncatlab is the closest I've found to a clear explanation. It seems like a fairly good article,...
user56834's user avatar
  • 12.9k
2 votes
0 answers
196 views

Simplest set of axioms and inference rules for first-order logic?

I'm interested in finding the "simplest" formulation of first-order logic. To be precise, what formulation of first-order logic has the fewest total axioms (or axiom schemas, henceforth just ...
WillG's user avatar
  • 6,467
0 votes
1 answer
121 views

How to write "the set of all walks of a graph" in formal logic notation?

I have this question on the CS stackexchange to figure out how to model "a walk of a graph" in a custom formal language. I think the problem is that there is not just one walk of a graph but ...
Lance's user avatar
  • 3,688
1 vote
0 answers
98 views

How do you formalize this reasoning?

There is this simple number theory problem which says "how many 4 digit numbers that are divisible by 3 and whose digits exclude 2, 4, 6 and 9 exist?" the solution is quite intuitive: each ...
Natrium's user avatar
  • 119
1 vote
1 answer
102 views

Axiom scheme for mathematical induction in formal axiom system for Peano Arithmetic

I'm reading the book "Gödel's incompleteness theorems" by Smullyan. (I found it online here: https://isidore.co/calibre/get/pdf/5823). In Chapter III he explains the Axiom System for Peano ...
Philipp's user avatar
  • 163
2 votes
1 answer
222 views

What is a precise definition of soundness?

I'm trying to better understand soundness, especially in contrast to semantic consistency. Here is what I've put together so far: Soundness: A theory is sound if all theorems are true under all ...
user2869495's user avatar
1 vote
0 answers
131 views

Is it possible to create a "hack-proof" system?

Various organizations, such as DARPA, have purported to create virtually "hack-proof" software systems using mathematical techniques such as formal verification. In short, the idea is ...
10GeV's user avatar
  • 1,331
0 votes
0 answers
36 views

Is there any technical, mathematical or logical, terminology for a set of propositions, all of which cannot be True at the same time.

As the question states, what is the technical term (if any) for a set of propositions which cannot all be true at the same time. That is to say, If there is a set, $A${x1, x2, x3, ... , xn} for which ...
ZarakshR's user avatar
0 votes
0 answers
78 views

Is it possible to list all hidden lemmas of a proof?

I'm studying Imre Lakatos' Proofs and Refutations for my master's thesis. Currently I address the concept of hidden lemmas, which I understand to mean unstated assumptions of a mathematical proof, ...
Agape's user avatar
  • 9
2 votes
1 answer
71 views

Beta Reduction Constraints

The definition of $β$ reduction is the following : $$(λx.M)N \rightarrow_{β} Μ[x∶=N] $$ So basically we stop treating $x$ as a bound variable and we perform substitution of the now free variable $x$ ...
RookieCookie's user avatar
3 votes
1 answer
154 views

Beta Reduction in Lambda Calculus

I came across the definition of beta reduction in Lambda Calculus which is : $$(λx.M)N \rightarrow_β Μ[\space x:= N \space]$$ under the constraint that the $FV(N)$ are still free after the ...
RookieCookie's user avatar

1
2 3 4 5 6