Hello! Is the forall x: an introduction to formal logic a good book on formal logic? I picked it up recently and would like to know this subs thoughts, thanks

I previously posted here, looking for advice about learning modal logic for somebody who hasn't studied maths since middle school. I started learning elementary logic today to build basics! And there are lots of confusing parts! So I was wondering if I there's anyone I could DM when I have questions.

something i see quite commonly when discussing the the limits of computing is that, for example, the halting problem indicates something about the hardness of determining whether any given machine halts. and while it is true that determining so can be quite impractically hard, bringing this up in a discussion about strictly the problem of undecidability itself is a red herring. computability is strictly concerned about the possibility of doing so, not on whether it is hard or not. conflating the two can lead to incorrect intuition about how undecidability manifests within computing, because undecidability within computing is simply not analogous to complexity or hardness.

for the following discussion we will be utilizing a partial halting recognizer:

𝓱p = (m: machine) -> {
  true: if m halts and m not depends on 𝓱p(m)->false
  false: otherwise
}

^{for more info on partial recognizers consider: r/logic/comments/1wzkua3/on_an_attempt_to_limit_undecidability_within}

-- a complex halting problem --

consider a machine that is possible for 𝓱p to recognize as halting:

// 2048 bit RSA modulus number
k = 0x95da00abc38f7a62884b1a13f985793265da5c41a0256131c10be07f2fb2c6b07c78930720c8e86eef5ad2e42abdb07c09edf5600aa5ac61d342a3146f6c472f21130582a8d5e62ddfc83abe88c0776f235998c6072fcdd00aae30ebffdae7f5d5aa97bffda0bc77cb5cb9cc73a5926a8bb8f8f9b5371e50071667fd5fb86a7e2f642e1dd982b8087445e5d7d4480cd799f8a95a244019bb2a4bc51d8392b15893acb460e999418caf1e65c158593465670c4f336a8112151e705cd275b01f8c83146ca8ddf347f99bce4bdadcdf8fa92b37f7266da472b1b8528639f6ce683312f83843031b39b0005454b540da3bdff94985541d94308f577e14d2f6f48131

hard_𝓱p = () -> {
  // loop if the sum of the digits, of the sum of
  // the prime factors, of k is odd
  [p,q] = prime_factors(k)
  if (sum_digits(p+q) % 2)
    loop
  else
    halt
}

the matter of 𝓱p(hard_𝓱p) is so complex to compute that it's not possible for us to decide with current theory/technology. we functionally do not know if hard_𝓱p halts or not, so we functionally do not know if 𝓱p(hard_𝓱p) returns true or false, and we will not know until quantum computing becomes viable enough if ever. we could hook all the computing power of the entire world together on cracking that one key and still not make a dent into computing the value of 𝓱p(hard_𝓱p) within a human lifetime.

such an example is not a proof of a limit to computability, cause given an unbounded computation those factors would provably be found within a finite time (as k is a real rsa key). computability doesn't care how hard the problem is, it is strictly concerned the possibility of computing a particular output, not whether it's pragmatically possible given real world computing constraints.

-- an impossible halting problem --

now consider a halting machine that is strictly not possible for 𝓱p to recognize as halting:

und_𝓱p = () -> 𝓱p(und_𝓱p) ? loop : halt

we can determine that und_𝓱p is unrecognizable to 𝓱p thru value injection analysis:

// inject true for `𝓱p(und_𝓱p)`
         () -> true ? loop : halt
// reduce static conditional:
         () -> loop

injecting true clearly leads to a non-halting machine so therefore 𝓱p must return false regardless of what the machine does. but since we aren't 𝓱p, we can determine the truthful semantic behavior of und_𝓱p

// inject false for `𝓱p(und_𝓱p)`
         () -> false ? loop : halt
// reduce static conditional:
         () -> halt

therefore und_𝓱p is a halting machine that is unrecognizable to 𝓱p, and it is not possible for 𝓱p to avoid this.

-- complexity vs computability in composition --

when the semantics of a particular machine is hard to compute, this complexity bleeds into any machine composed with it in the execution path. for example: consider the higher order machine wrap which constructs a new machine composed from the input by appending a noop after executing the input machine. in base turing machines, a noop is just an excess state transition.

wrap = (m: machine) -> 
  () -> { m(); noop }

the extra noop does not affect whether this machines halts or not, so the complexity of computing whether wrap(m) halts or not is entirely dependent on how hard it is to compute whether m halts or not. so the complexity of computing 𝓱p(wrap(hard_𝓱p)) is the same as just 𝓱p(hard_𝓱p), which is impossible with today's theory/technology.

but when the semantics of a particular machine is impossible to recognize, does this impossibility then bleed into machines composed of it? one might think that if m is not possible for 𝓱p to recognize, then surely wrap(m), which is the same machine just with an excess state transition at the end, would similarly be impossible to recognize for 𝓱p...

this is not the case. und_𝓱p and wrap(und_𝓱p) are different machines that are therefore different input to 𝓱p and can have different output. the unrecognizable nature of the input und_𝓱p is due to the paradoxical dependency on strictly the input und_𝓱p, not wrap(und_𝓱p). so while 𝓱p(und_𝓱p)->false, it is still possible for 𝓱p(wrap(und_𝓱p))->true. we can demonstrate how 𝓱p comes to this recognition thru value injection analysis:

wrap(und_𝓱p) = () -> { 
  und_𝓱p()
  noop
}

// expand und_𝓱p
() -> { 
  (() -> 𝓱p(und_𝓱p) ? loop : halt)()
  noop
}

// run 𝓱p(und_𝓱p) to -> false, inject value:
() -> { 
  (() -> false ? loop : halt)()
  noop
}

// reduce static conditional
() -> { 
  (() -> halt)()
  noop
}

𝓱p(() -> halt)->true and 𝓱p(noop)->true so therefore 𝓱p(wrap(und_𝓱p))->true and there's no paradox stopping it from returning so. the machine wrap(und_𝓱p) is strictly independent of 𝓱p(wrap(und_𝓱p)) so somewhat counter-intuitively: there is nothing unrecognizable to 𝓱p about wrap(und_𝓱p) being a halting machine. recognizing what und_𝓱p does within the context of wrap(und_𝓱p) is not the same problem of recognizing und_𝓱p on it's own. computability and complexity are neither the same thing, nor even analogous in nature.

do note that wrap is not likely to be some kind of panacea that will help us produce a total halting decider. a more "clever" halting machine unrecognizable to 𝓱p, can also make the wrapped version of itself unrecognizable:

und_wrap_𝓱p = () -> {
  if (𝓱p(und_wrap_𝓱p)) loop
  if (𝓱p(wrap(und_wrap_𝓱p))) loop
  halt
}

^{i would like to thank u/we_think_is_cool for the discussion that inspired this post}

A friend and I are going to read through This book by Smullyan. Taking it reasonably seriously with meetups online at least every 2 weeks.

I want to do a PhD in logic and analytic philisophy and I want to stay in academia after as a researcher. But I am afraid of AI taking over the field. What are your opinions on this?

I want to learn modal logic for philosophical and formal purposes. However, I don't have basic knowledge of it. I haven't studied mathematics since middle school. Thus, I feel very lost and have no idea how to get started! Any advice? Book recommendations & video recommendations would also be appreciated

Hi there!

I'm finishing my bachelor in philosophy and my end-of-degree project is gonna focus on the epistemology of logic, in particular, on how can we account for a justification of the validity of our basic belief-forming methods (modus ponens, for example). I've been focusing on Boghossian's work, that gives an inferentialist answer to that question –MPP is valid for everyone that has the concept "if... then", for it is a precondition of having that concept to accept its validity–. I'm aware that there is a similar view of semantics, proof-theoretic semantics, that is currently being studied in a more formal academic environment. Any bibliographical suggestions? Also, if you think there are other topics that could help me introduce myself in the issue, it will be great to know.

Thanks a lot :)

In an essay, why is one's answer better/more appropriate than another's?

We might argue one does a better job of answering the question, is more relevant or even provides reason that bears greater utility, etc...

In a way, I think this is like the qualitative version of decision theory: why is one result or choice better than another? However herein lies the problem. We do not assign numerical values to answers in essays (in the way we can with probability or reward functions), so what exactly are we judging here? It's not reason, clearly, because one answer could provide excellent reasoning and still be a less accurate/appropriate answer to our question.

What i'm not looking for here is for someone to say, 'oh it's subjective'. This is the common response.

A question (a poor example albeit); If I were to say provide me with the name of something yellow. One person says a supermarket-appropriate lemon and the other says a cream sofa. We could quarrel that the lemon may in rare cases be a little green, but we can all agree that the answer is 'better/more appropriate' than the latter.

So what exactly is this reasoning, this correctness, this ability to appropriately answer a question that is 'better' than another's.

Would love to hear your thoughts on this across the board!

Thank you for reading.

Suppose we consider Classical Propositional Logic under some axiom set. For example, I'll pick Jan Lukasiewicz's preferred axiom set (he uses this set it in two of his books, including his introductory textbook... not in smaller papers):

{CCpqCCqrCpr, CCNppp, CpCNpq}

All lower case letters of the Latin alphabet are variables.

The definitions for other connectives go:

Apq defined as CNpq (logical disjunction defined)
Kpq : NCpNq (conjunction)
Epq : NCCpqNCqp (equivalence)
Dpq : CpNq (joint denial)

Now consider an arbitrary list of proved tautologies

[x¹, x², ... xⁿ ]

For each element a sufficiently powerful machine could produce a conjunction or equivalence to make another list such as

[Kx¹x¹, ..., Kxⁿxⁿ]

or

[Ex¹x¹, ..., Ex¹x¹]

Each element of either those lists can get corresponded back to the original list. Consequently, we have a one-to-one correlation between the set of proved tautologies which are not negations, and the set of tautologies which are negations. It follows by mathematical induction, that

Meta-Lemma: The cardinality of the tautologies which have the type 'negation' or 'N' is equal to the cardinality of the tautologies which have the type 'conditional' or 'C'.

Therefore:

Meta-Theorem: If the cardinality of conditional tautologies is infinite (which it must be if tautologies can have an arbitrary length), the cardinality of negation tautologies is infinite also.

That might seem to conclude the matter, but since we've assumed the natural numbers, I think there exists a catch to what we can consider as reasonable to believe. If we consider the natural numbers, there always exists a natural number greater than what we have encountered so far. For any list of natural numbers, there exists a much longer finite list of natural numbers. Thus, in terms of what it ends up reasonable to believe, we could write as some have done:

"all numbers are small."

which of course isn't strictly speaking true, but expresses the sense of what numbers must be like if we retain our notion of size in the natural numbers for most of them. Maybe better:

"Most numbers are much bigger than anyone has ever thought or ever will think."

Now I ask that you notice that negations which are tautologies also have a similar property. They are longer than tautologies used to derive them. And even more significantly so, once we start considering so-called equivalences (which again, are negations). But, at least I think, many of us have the vast majority of our encounters with positive tautologies. What textbooks even prove a single tautology which is a negation (Lukasiewicz's does), let alone prove an equivalent amount of negation tautologies to non-negation tautologies?

To get a better sense of the truth we would need to think something like:

"If we had to pick between negation tautologies and positive tautologies for what exists, we would logically pick negation tautologies." At least if the tautologies we haven't seen are more likely to be longer than what we have seen.

Negation tautologies have many uses, as automated theorem proving has shown. But are they just as useful as the equi-cardinality meta-theroem above suggests?

At the very least requiring that tautologies have a finite length specified in advance makes finding negation tautologies less likely. Though maybe instead every modern logician is a fool who didn't emphasize negations enough (this last sentence is a joke).

I just started taking this university course on logic since I do philosophy, and I tried putting my reasoning on a piece of paper and something just feels wrong. Can anyone help me?

Oh I didn’t write the numbers on the left (idk how to translate them in English) but I assume they are respectively

1,2 5)
3 6)

The Saul Kripke Center invites submissions for Logic in Metaphysics: Classical and Non-Classical Approaches, a two-day conference on the role of logic in contemporary metaphysics. This conference will showcase work that uses, develops, or critically examines both classical and non-classical logical frameworks in addressing metaphysical questions. We welcome papers addressing the general question of what logic can or should contribute to metaphysical inquiry as well as particular cases in which metaphysical theorizing appears to support, require, or resist departures from classical logic. Topics may include, but are not limited to, realism and antirealism, indeterminacy and vagueness, impossible worlds and counterpossibles, dialetheism, future contingents, and non-classical reconstructions of classical metaphysical views (e.g., logical atomism or verificationism). Papers defending classical approaches are welcome.

Can independent, basic, or regular premises receive support? I understand that they directly and independently support the next conclusion.

EDIT:I think I understand. I was thinking of it as Only(If (A)). That is the Only operator is applied to the sufficient condition If(A) but formal logic is asking me to think of it as Only If(A). That is, Only If() is it's own operator. It is not an Only() operattor applied to If(A) operator.

"If A then B" means "All A is B" but other things can still be B like C,D,E,etc...

Why doesn't "Only if A then B" mean "All A is B" but now C,D,E,etc can no longer be B, hence Only All A is B. Why does this "only" operation exclude All A all of a sudden?

Feel like if we were building on top of "If A then B" by adding "Only" to "If A", that would be the most intuitive way of thinking about it because it still satisfies "All B is A" as well.

But then this would require some extra operators like "Some"

"Only If Some A then B"

A kripke frame (W, R) is reflexive iff every instantiation of □p → p is valid in it. (W, R) is transitive iff every instantiation of □p → □□p is valid in it.

I’ve been trying to find axiom schemes for other order properties like density and upward directedness, but it’s been tough (please DON’T tell me anything about these examples! I want to figure out if it’s possible on my own, and I have a course planned out!). I guess one difference is that these other properties involve existential statements (so i imagine the dual modal operator will show up), whereas the previous examples were all universal. But at the end of the day my biggest struggle is intuitively seeing how the formulas relate to the order properties. I don’t think this is helped by the fact that to prove an axiom scheme implies an order prop, I’ve only been able to prove the contrapositive: assume the order prop fails and then cook up a satisfaction relation to make an instance of the scheme fail.

Does anyone have any advice for how to intuitively see the relationship between axiom schemes and order properties? And if off the top of your head you have any good examples/challenges please feel free to share them!

In a recent YouTube video math mathematician hannah fry has come up with some mathematical rules and representations for how a faithful would best play the game traitors to identify the traitors.
She has devised logic with weights applied to each which are added to an individual player’s total tally each time they make a specific move, with the resulting number indicating, if a high number = more likely to be a traitor, low number less likely to be a traitor.

The rules are as follows.
Casting a ‘burn vote’ +0.47
Voting for a banished traitor +0.33
Voting for a banished traitor despite never voting for them before +0.4
Does not vote for a banished traitor -1.28
If someone appears on a banished traitors voting record -1.69

Now, what I want to focus on is how people are able to formulate/come up with this logic/these rules specifically. Coming up with specific rules about a game or situation is absolutely key in our ability to play the game and out manoeuvre other players. Yet some players are better at formulating these rules than others. I want to understand why some people are better at forming these rules and spotting these patterns than others. This can be applied to so many walks of life, it is the absolute essence of problem solving.

What areas of academia are relevant for forming correct rules about a given situation, recognising behaviours, actions, and applying them to a structure, a game, or a situation.

I note becuase in social politics there are ways of winning/playing the game of power and deception, and some people play better than others by knowing rules others don’t, some people make social plays & deceptions others do not recognise, but how are these rules devised is the key question

I'm just starting to study logic and am having trouble understanding this. For context, it's in my math textbook. After this topic, the book moves on to sets and then functions

Yo so this logic shit seems cool to me and I wanna learn it (preferably free).What would be the best way?Know it might seem like this post is satire but I genuinely want to learn.

hi all, this is related to my work from another post: on the nature of undecidability within computing and refuting the church-turing thesis. when i started writing this post it was going in a very different more optimistic direction, but things turned for the worse as i refuted one of the more promising points in my draft...

in that draft i invent a new form of classifier machine in an attempt to get around undecidability paradoxes that are found within computing due to the inherent possibility of self-referential paradoxes. like the canonical und = () -> halts(und) ? loop : halt, these machines create necessarily paradoxical dependencies with their logical structure. in this example und is either a halting machine that depends on halts(und) -> true or und is a looping machine that depends on halts(und) -> false. which it is isn't specified because halts as envisioned in that example is underspecified and cannot be implemented as a machine. to contrast with my proposal i will also detail what conventional theory already discusses, with examples for the circle-free problem since those will be more relevant moving forward.

-- total decider --

a total decider returns for all input, correctly maps the input, doing so with coherent dependencies on 𝓓(m) (if applicable):

𝓓 = (m: machine) -> {
  true: m is circle-free and not depends on 𝓓(m)->false,
  false: m is circular and not depends on 𝓓(m)->true,
}

consider undecidable machine und_𝓓:

und_𝓓 = () -> 𝓓(und_𝓓) ? halt : loop { output 1 }

und_𝓓 is either a circular machine when dependent on𝓓(und_𝓓)->true or und_𝓓 is a circle-free machine when dependent on 𝓓(und_𝓓)->false ... neither of which is a form of machine that 𝓓 can decide. therefore 𝓓 cannot be implemented as specified, as it does not handle all forms of input.

-- total recognizer --

a total recognizer returns true for all circle-free input, but may diverge (and block indefinitely) on some circular input. when it does return the dependencies are coherent (if applicable):

𝓓r = (m: machine) -> {
  true: m is circle-free and not depends on 𝓓(m)->false,
  false: m is circular and not depends on 𝓓(m)->true,
  diverge: m is otherwise circular
  // not specified to diverge for _any_ circle-free machines
}

𝓓r is more paradox resistant than 𝓓 because diverging can prevent certain incoherent dependencies from arising. consider the machine div_𝓓r:

div_𝓓r = () -> 𝓓r(div_𝓓r) ? halt : loop { output 1 }

𝓓r(div_𝓓r) can diverge to align with it's specification but it's not possible to build this because with parallel execution u can construct a circle-free machine that depends on 𝓓r diverging, which this decider has no specification for and is therefor unimplementable. consider the machine und_𝓓r:

und_𝓓r = () -> {
  dr = steppable(() -> 𝓓r(und_𝓓r))
  loop {
    dr.step()                   // run 𝓓r for one step/transition
    if (dr.output() == true)    // if 𝓓r outputs true, halt
      halt
    else
      output 1
  }
}

total deciders and total recognizers are the two forms of classifiers acknowledged in textbook computing theory, where total deciders do not exist, and total recognizers only exist for semi-decidable sets (including halting machines, but not circle-free machines). nothing i've written so far disagrees with this. it's worth noting that "partial deciders" such as (m) -> true is just internet bs hallucination, those are not any form of semantic classifier.

-- partial recognizer --

a partial recognizer returns true for all circle-free input with a coherent (or no dependency) on 𝓓p(m), but will mix certain circle-free machines in with false that have an incoherent dependency on 𝓓p(m), ei are dependent on 𝓓p(m) -> false

𝓓p = (m: machine) -> {
  true: m is circle-free and not depends on 𝓓p(m)->false,
  false: m is circular or
        (m is circle-free and depends on 𝓓p(m)->false),
}

consider the machine und_𝓓p:

und_𝓓p = () -> 𝓓p(und_𝓓p) ? halt : loop { output 1 }

𝓓p(und_𝓓p) cannot be true as that would cause und_𝓓p to be circular violating it's specification. but unlike in the case of 𝓓, 𝓓p(und_𝓓p) returning false causing und_𝓓p to be circle-free is still aligned with it's specification for returning false on circle-free input that is dependent on it returning false. so this case is technically decidable, and won't gum up downstream logic which might depend on the value, even if it doesn't manage to recognize the circle-free machine. we will call a machine like und_𝓓p unrecognizable to 𝓓p, not undecidable.

furthermore due to 𝓓p mixing in both circular and circle-free machines in with it's false return, 𝓓p does not recognize any machine with false. this is a start contrast to total deciders and total recognizers which recognize machines with both true and false outputs. a total decider is defined to totally recognize a set with true, and totally recognize the complement with false, which is just not logical feasible on turing machines due to the possibility of paradoxical dependencies in such a recursively enumerable set of computations. a total recognizer still totally recognizes a set with it's true return, but only recognizes a subset of the complement with it's false return, while presumably diverging any there are unrecognizable to it, and is logically feasible for semi-decidable problems like halting. while the defined partial recognizer of this post recognizes a particular subset of machines with it's true output, no machines with it's false return, but never has to diverge.

-- why the interest in 𝓓p? --

(1) despite turing wrongly conflating the two, it is not actually necessary to correctly identify all circle-free machines in order to enumerate all possible output sequences. infinite machines compute any given sequence, and only one is needed to compute any given possible output sequence. so despite only being able to enumerate a subset of all circle-free machine, one may wonder whether 𝓓p can identify a turing-complete subset of machines.

and even if it doesn't, a next question arises: what kind of output sequences are strictly computed by circle-free machines dependent on 𝓓p(m)->false vs those which can be computed by machines which either depend on 𝓓p(m)->true, or have no dependency at all on 𝓓p(m) at all. and quite pointedly: should we actually care about those that are missed?

(2) despite only being a partial recognizer in respect to all circle-free machines, 𝓓p is a non-trivial total decider in it's own right, namely for those machines which are circle-free and do not depend on 𝓓p(m)->false. this alone would refute rice's theorem, and would be quite the revelation. this aspect i have not explored much.

-- a failed attempt to place a limit on undecidability --

for any recognizer proposing to totally identify a set of circle-free machines, we can construct a diagonal across that recognizer:

𝓗 = (d) -> 
  () -> loop (n=0, r=0; true; n++) {
    if (d(n) == false) continue      // skip invalid, circular, or paradox machines
    output sim(n,r)                  // simulate machine to r-th output and output
    r++                              // count circle-free machines
  }

unfortunately 𝓗(𝓓p) is not recognizable by 𝓓p due to the same infinite recursion that stumped turing in the famous §8 of on computable numbers, which would cause 𝓗(𝓓p) to get stuck at sim(𝓗(𝓓p),r) for some r. we can however construct a diagonal across 𝓓p that is recognizable by 𝓓p, avoiding that particular infinite recursion:

𝓗p = () ->
  loop (n=0, r=0; true; n++) {
    if (𝓓p(n) == false)
      continue
    if (n == 𝓗p)      // output digit for itself on the diagonal
      output 0
    else
      output sim(n,r)
    r++
  }

this unfortunately can be diagonalized by an anti-machine. for any machine that exists, an anti-machine will also exist:

anti = (m) -> 
  () -> loop (r=0; true; r++) output 1-sim(m,r)

the anti-machine anti(𝓗p) will not be recognizable by 𝓓p as this would become circular due to the same infinite recursion. unfortunately there's no way to "fix" this diagonal, as unlike 𝓗p we cannot construct a machine that will ever output it's own anti-output to machine anti(𝓗p) and still be recognizable like 𝓗p.

but as demonstrated by anti, this machine form a computable relationship between those which is recognized by 𝓓p, which means we can enumerate it alongside those recognized by 𝓓p, and perhaps might catch the machines missed by 𝓓p alone:

𝓔 = () -> loop (n=0; true; n++) {   // iterate over all possible machines
  if (𝓓p(n) == false) continue      // skip invalid, circular, or paradox machines
  output n                          // output machine
  output anti(n)                    // output anti-machine
}

we can then construct a circle-free recognizer based on 𝓔:

𝓓e = (m: machine) -> loop (n in 𝓔()) {
  if (m < anti(n))      // since 𝓔 is in-order we can return false once at
    return false        //   machines too complex to be m 
  elif (m == n)
    return true
}

as much as i was excited at the prospect, this does not manage to capture all the circle-free machines missed by 𝓓p. in this case 𝓓p can't even recognize a circle-free machine equivalent to the diagonal 𝓗(𝓓e), as the machine anti(machine) enumeration befuddles an attempt to do so. the closest 𝓓p recognizable machine to 𝓗(𝓓e) will invariable be off for any machine computing its anti-sequence:

almost_𝓗e = () -> {
  r = 0
  loop (m in 𝓔()) {
    if (m == almost_𝓗e)
      output 0
    elif (m == anti(almost_𝓗e))  // anti-identity check required to be circle-free
      output 1                    // output what will be an anti-digit for the anti-machine
    else
      output sim(m, r)
    r++
  }
}

anti(almost_𝓗e) is also a circle-free machine, but it will not be a total anti-diagonal as it the bit it outputs for itself on the diagonal (and any machine which computes the same sequence) will be the output for the machine, not the anti-output.

-- what next? --

despite my current failures to limit undecidability, this was a necessary failure in getting to this point of expressing 𝓓p so precisely based on the dependencies. that particular description was only a result of my discussion with u/OpsikionThemed, who i will thank again for actually engaging with genuine consideration... something that is tragically rare on the internet.

with this description can i precisely define the root cause of 𝓓p failing to recognize some machine like und_𝓓p: an incoherent dependency, where the circle-free execution of und_𝓓p necessarily follows from 𝓓p(und_𝓓p)->false.

we can constructively prove the language of circle-free machines unrecognizable to 𝓓p must be turing-complete, as any circle-free machine m recognizable by 𝓓p has an associated machine und(m) that is unrecognizable to 𝓓p:

und = (m: recognizable circle-free machine) -> {
  und_m = () -> {
    if (𝓓p(und_m)) halt   // construct incoherent dependency
    output m()            // und_m outputs the same as m
  }
  output und_m
}

however even if the language recognizable by 𝓓p isn't totally turing-complete ... why do we actually care about those machines which depend on 𝓓p(und_𝓓p)->false? perhaps there is an entirely valid and potentially transformative notion of effectively turing complete language that performs all the computations we're interested in. there is no practical reason to build a circle-free machine that is dependent on being unrecognizable to 𝓓p. and the language of circle-free machines unrecognizable to 𝓓p may not even contain output of academic value, like those open unanswered questions in number theory.

for example consider a machine that computes in accordance with the collatz conjecture:

collatz = (n: ℕ) -> {
  if (n == 1)
    output 1
  elif (n%2 == 0)
    output collatz(n/2)
  else
    output collatz(3*n + 1)
}

collatz_conj = () -> loop (n=0; true; n++) output collatz(n)

if collatz_conj is a circle-free machine then the collatz conjecture is true. from this construction it doesn't appear that the collatz conjecture being circle free would depend on 𝓓p(und_𝓓p)->false, so if it is true, then this machine would be recognizable by 𝓓p. if not then it ought to be recognizable by a complement circular partial recognizer 𝓓p', as collatz_conj also does not have a dependency on 𝓓p'.

-- request for help --

what i'd like to ask this group is help or inspiration on how i might prove that 𝓓p exists. i suppose a proof that it cannot be refuted via a conventional diagonalization proof would be a great start on whether it might exist, but i suppose a non-constructive proof like such isn't great at demonstrating the certain existence of an algorithm we haven't yet built. and a constructive proof would require actually building it ... which is a research question far outside the scope of a single person, or at least that's how it seems atm