Skip to main content
MathOverflow

Return to Question

added 8 characters in body
Source Link
Zuhair Al-Johar
Zuhair Al-Johar
  • 11.3k
  • 1
  • 13
  • 47

[The question has been edited]

Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:

$T + \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$$T + \\ \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$

is consistent.?

Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.

In other words, can $T$ can be consistently extended by its own completeness and consistency.?

[The question has been edited]

Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:

$T + \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$ is consistent.

Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.

In other words, $T$ can be consistently extended by its own completeness and consistency.

[The question has been edited]

Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:

$T + \\ \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$

is consistent?

Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.

In other words, can $T$ be consistently extended by its own completeness and consistency?

added 28 characters in body; edited title
Source Link
Zuhair Al-Johar
Zuhair Al-Johar
  • 11.3k
  • 1
  • 13
  • 47

Is Can there be an effectively generated consistent theory that extends PA and provesbe consistently extended by its own internal completeness and internal consistency?

[The question has been edited]

Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:

$T \vdash \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$$T + \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$ is consistent.

Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.

In other words, $T$ proves that it is internally both completecan be consistently extended by its own completeness and consistent?consistency.

Is there an effectively generated consistent theory that extends PA and proves its own internal completeness and internal consistency?

Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:

$T \vdash \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$

Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.

In other words, $T$ proves that it is internally both complete and consistent?

Can there be an effectively generated consistent theory that extends PA and be consistently extended by its own completeness and consistency?

[The question has been edited]

Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:

$T + \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$ is consistent.

Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.

In other words, $T$ can be consistently extended by its own completeness and consistency.

Post Undeleted by Zuhair Al-Johar
Post Deleted by Zuhair Al-Johar
Post Undeleted by Zuhair Al-Johar
Post Deleted by Zuhair Al-Johar
Post Undeleted by Zuhair Al-Johar
Post Deleted by Zuhair Al-Johar
Source Link
Zuhair Al-Johar
Zuhair Al-Johar
  • 11.3k
  • 1
  • 13
  • 47

Is there an effectively generated consistent theory that extends PA and proves its own internal completeness and internal consistency?

Can we have an effectively generated consistent theory $T$, that extends $\sf PA$, such that:

$T \vdash \forall \mathcal S \, [\exists x: \operatorname {Proof}_T(x, \ulcorner \mathcal S \urcorner) \oplus \exists y: \operatorname {Proof}_T(y, \operatorname {neg}(\ulcorner \mathcal S \urcorner))]$

Where "$\operatorname {neg}$" is Rosser's negation function. and "$\oplus$" is exclusive disjunction.

In other words, $T$ proves that it is internally both complete and consistent?